Issues

• z3 before 5.1.0 reports error columns one too high after a comment line

  bug
  smtlib/jSMTLIB#196 · Filter by author davidcok opened on Nov 1, 2026

• SMTInterpol hangs on a repeated declare-sort-parameter (interactive mode)

  bug
  smtlib/jSMTLIB#195 · Filter by author davidcok opened on Nov 1, 2026

• Small follow-ups: solver list check, seed handling, start-mode options, --port, pipelined stub tests

  enhancement
  smtlib/jSMTLIB#194 · Filter by author davidcok opened on Nov 1, 2026

• yices2 answers get-value on a quantified term with ??? (not an SMT-LIB value)

  bug
  smtlib/jSMTLIB#193 · Filter by author davidcok opened on Nov 1, 2026

• Remaining FIXMEs from the FIXME review

  smtlib/jSMTLIB#192 · Filter by author davidcok opened on Nov 1, 2026

• Error message for a function symbol used as a term (A34)

  smtlib/jSMTLIB#191 · Filter by author davidcok opened on Nov 1, 2026

• Move the adapters' duplicated start-failure handling into AbstractSolver

  smtlib/jSMTLIB#190 · Filter by author davidcok opened on Nov 1, 2026

• alt-ergo: verify the --timeout/--timeout-total mapping to --timelimit

  smtlib/jSMTLIB#189 · Filter by author davidcok opened on Nov 1, 2026

• INumeral.intValue() silently wraps numerals >= 2^31

  smtlib/jSMTLIB#188 · Filter by author davidcok opened on Nov 1, 2026

• Document node equality semantics and the canonical form of compound attribute values

  smtlib/jSMTLIB#187 · Filter by author davidcok opened on Nov 1, 2026

• alt-ergo: strict readings of logic definitions still recorded as conforming goldens

  smtlib/jSMTLIB#186 · Filter by author davidcok opened on Nov 1, 2026

• SMT-LIB keyword syntax is ambiguous: :⟨simple_symbol⟩ vs. the example :56

  smtlib/jSMTLIB#185 · Filter by author davidcok opened on Oct 31, 2026

• Local test environments: known failures under Docker and Windows emulation

  smtlib/jSMTLIB#184 · Filter by author davidcok opened on Oct 31, 2026
  1

• z3-4.3.2 adapter can wait indefinitely if check-sat answers only 'success' lines

  smtlib/jSMTLIB#183 · Filter by author davidcok opened on Oct 31, 2026

• Pipelined runs: out-of-step solver output can be reported differently or not at all, depending on timing

  smtlib/jSMTLIB#181 · Filter by author davidcok opened on Oct 31, 2026

• Printer: consistent spacing in printed lists

  enhancement
  smtlib/jSMTLIB#180 · Filter by author davidcok opened on Oct 31, 2026

• Possible nondeterministic output after an error ends yices2, cvc5 or bitwuzla

  smtlib/jSMTLIB#179 · Filter by author davidcok opened on Oct 30, 2026
  1

• Type checker treats sort parameters as new sorts, not type variables

  smtlib/jSMTLIB#178 · Filter by author davidcok opened on Oct 30, 2026

• Dead code from the 2026-10-27 coverage assessment: remove or annotate

  smtlib/jSMTLIB#177 · Filter by author davidcok opened on Oct 29, 2026
  1

• Inventory of skipped tests (.skip files): reasons, and which could become goldens

  smtlib/jSMTLIB#176 · Filter by author davidcok opened on Oct 29, 2026
  1

• Solver BUG: z3-4.3.1 answers unknown when proofs and unsat cores are both enabled

  smtlib/jSMTLIB#175 · Filter by author davidcok opened on Oct 28, 2026

• Audit: illegal structures constructible through the API (construction-time prevention or type-check errors)

  smtlib/jSMTLIB#174 · Filter by author davidcok opened on Oct 27, 2026
  1

• DESIGN: the sexpr package name, and solver commands jSMTLIB does not model (from #172)

  smtlib/jSMTLIB#173 · Filter by author davidcok opened on Oct 27, 2026

• DESIGN: where the AST holds raw s-expressions, and how they relate to typed SMT-LIB structures

  smtlib/jSMTLIB#172 · Filter by author davidcok opened on Oct 27, 2026
  1

• Solver BUG: smtinterpol-2.5 keeps datatype constructors and selectors across reset-assertions

  smtlib/jSMTLIB#170 · Filter by author davidcok opened on Oct 26, 2026