jSMTLIB 0.14.0

Changes since the 0.13.0 release.

Time limits

• New IResponse.IFactory#timeout(). A solver ended by its whole-run time limit
  (SMT.Configuration#timeoutTotal) now answers timeout() for the command that
  hit the limit and for every later one. z3 (-T:) answers timeout and exits;
  cvc5 (--tlimit) reports on stderr and aborts; each adapter recognizes its own
  solver's report (isTimeLimitResponse). The limit runs on the wall clock, so it
  can end a solver between commands; the next request -- including get-value
  and the other commands that send directly -- then recovers the report from the
  process's unread output (SolverProcess#unreadOutput).
  (OpenJML/OpenJML#1029)
• z3: a query stopped by the per-query limit reports reason timeout, as cvc5
  does, where z3 4.16/5.1 in incremental mode say canceled.
  (OpenJML/OpenJML#1022)
• yices2's --timeout applies per check-sat (observed with 2.7.0);
  smtinterpol and alt-ergo apply the limit per query; bitwuzla's whole-run
  report is unverified.

Solver adapters and API

• cvc5 is stopped after a parse error: when run interactively it neither
  processes further input nor reliably exits, so later commands or exit()
  waited forever. requireOptionEnabled reports a failed get-option query as
  that error, not as the option being off.
• Solver_z3_4_3.get_value returns structured values like the other adapters,
  so z3 4.3 prints model values exactly as newer z3 versions do.
• Parser.parseScript reports a missing closing parenthesis instead of looping.
• The command line exits with code 2 for a crash (an uncaught exception),
  distinct from 1 for rejected input, also when several files are processed.

Logics report

logics-report.py, a manual all-platform tool:

• Combines the probe results of every platform into one report, with a
  cross-platform consistency check, a (default) row and ALL, and outputs as
  Markdown (CI summary), LaTeX (the tutorial's "SMT-LIB Logics supported by
  solvers" appendix) and HTML (the published page).
• Probe fixes: stdin is closed, alt-ergo is invoked with its SMT-LIB front end,
  the set-logic response is graded rather than the last line, partial output
  is kept on a probe timeout, a solver that times out on three consecutive rows
  is no longer probed, and an unusable binary is reported once rather than as
  45 disagreements.

Tests

• New: WholeRunTimeoutTests, ImmediateExitSolverStoppedAfterErrorBugTest,
  ParseScriptMissingCloseParenBugTest.
• Goldens updated for the version bump and z3 4.3's get-value format.
• Full suite: OK (11262 tests); CI passes on all five platforms.