jSMTLIB 0.16.0

Changes since the 0.15.0 release.

This is mostly a bug fix and usability cleanup release.

Command line

• A file argument of - reads standard input as a file (#138): no prompts, errors show the source line, --abort stops the run, and --pipeline applies. A repeated - reads nothing more. Without -, standard input is interactive as before.
• --pipeline given with input it does not apply to (interactive standard input, --port) now prints a warning instead of being silently ignored.

Solver output

• A bare word that cannot answer the command sent is no longer taken as a response (#134). If the solver has stopped, the command gets (error "The solver stopped without a response to: <command>"); otherwise (error "Unexpected response from the solver: <text>"). Examples are a crash banner's first word, or bitwuzla 0.9.1 aborting on a define-fun whose body is a numeral (#112; reported upstream as bitwuzla/bitwuzla#231, fixed there but not yet released). An empty reply is still accepted, and get-option and echo may still be answered by any symbol.
• A solver reply that is not SMT-LIB gives one error instead of two (#148). The lexer no longer reports errors itself; the parser reports them, once per bad command, with their positions. A script command containing two bad tokens may now report only the first.

Library

• A .command property works with every adapter (#147). cvc5, bitwuzla, z3 (Solver_z3_recent), z3-4.3.2, simplify and alt-ergo previously failed with "Could not find an appropriate constructor". The command is used as given, so it must include the flags the adapter relies on (for example cvc5's --print-success).
• SMT.Configuration.createSolver's resolution rules are moved into SolverResolver (#123), which is public for its tests but internal. createSolver's signature and behavior are unchanged.
• The generic s-expression printer and IVisitor.TreeVisitor are iterative, so deeply nested input no longer overflows the stack (#132).
• Behavior change for API clients: the Lexer no longer writes lexical errors to the log. Parser.parseCommand and parseScript still report them. A client that calls other Parser methods directly gets them as a ParserException, or as an error token where one is accepted.

Tests, CI and documentation

• .tst tests can use a stub solver with canned replies (a Name.tst.stub file) for solver behavior that real solvers cannot be made to show on demand (#145).
• The ; OPTIONS: directive accepts quoted arguments (#109). --verbose in a directive is safe (#110), and the bash runtest honors directives (#137).
• A script test can skip itself, so make test-only passes (#135). all-statistics.scr now checks yices2.
• Script tests that start jSMTLIB with a bare java command are now covered by coverage runs (#124).
• New tests for code that coverage found unreached (#140).

Full suite: 12088 tests pass locally (macOS x86_64); the suite passes in CI on Linux x86_64 and ARM64, macOS ARM64 and x86_64, and Windows (release commit a7dddb1).