While implementing a proper scanner for vim-smt2's auto-formatter I stumbled over minor issues with the testcase originally provided by you @krobelus. The issues are SMT-LIB specific, so if you aim for a generic Lisp formatter they might not be problematic for you at all. They caught me by surprise so I wanted to make you aware of them 😅

• The following line should probably not be considered as properly formatted:
  

  smtfmt/smtfmt.py

  Line 225 in da3ac23

  (list (list (fun) (number 0.0.0.0:5900) atom))

  
  Here, 0.0.0.0:5900 is understood as a single symbol and correspondingly formatted as such. However, according to the SMT-LIB token specification, these are three separate tokens

  pos  len            kind  lexeme
   26    3         decimal: 0.0
   29    4   simple_symbol: .0.0
   33    5         keyword: :5900

so the formatter should probably separate them by whitespace and consider putting them on separate lines.

• While the above example features three tokens that are treated as a single token, it can also happen that the formatter treats a single one as a bunch of tokens. For example, this happens when we have quoted symbols such as | this is a single symbol |.

There are some more cases that the formatter does not account for so I suggest just skimming the token specification to decide whether the edge cases are worth being "fixed" for smtfmt.