Issues

• Campaign observations: unchecked proof steps, unresolved allocations and instrumentation limits

  vprover/vampire#1007 · Filter by author shalashaska117 opened on Sep 25, 2026

• Problem::addUnits counts existing clauses again when its Property cache is valid

  vprover/vampire#1006 · Filter by author shalashaska117 opened on Sep 25, 2026

• SMT finite-model enumeration tries sizes above a detected sort maximum

  vprover/vampire#1005 · Filter by author shalashaska117 opened on Sep 25, 2026

• An empty --decode argument triggers a Debug assertion

  vprover/vampire#1004 · Filter by author shalashaska117 opened on Sep 25, 2026

• Timer thread creation failures cause an uncaught std::system_error

  vprover/vampire#1003 · Filter by author shalashaska117 opened on Sep 25, 2026

• Native SAT derivation lines corrupt smtcheck and property proof output

  vprover/vampire#1002 · Filter by author shalashaska117 opened on Sep 25, 2026

• SimpleCongruenceClosure::getModel retains the first instance in a static comparator

  vprover/vampire#1001 · Filter by author shalashaska117 opened on Sep 25, 2026

• GROUND abstraction generates and activates a non-ground constraint

  vprover/vampire#1000 · Filter by author shalashaska117 opened on Sep 25, 2026

• CONSTANT abstraction misses an identical rational constant in term-index retrieval

  vprover/vampire#999 · Filter by author shalashaska117 opened on Sep 25, 2026

• StringUtils replaceChar and sanitizeSuffix return stale bytes after an embedded NUL

  vprover/vampire#998 · Filter by author shalashaska117 opened on Sep 25, 2026

• StringUtils numeric predicates accept the empty string

  vprover/vampire#997 · Filter by author shalashaska117 opened on Sep 25, 2026

• Valid empty quoted SMT-LIB symbols trigger Debug assertions

  vprover/vampire#996 · Filter by author shalashaska117 opened on Sep 25, 2026

• Translating rational or real $round to Z3 fails with a sort error

  vprover/vampire#995 · Filter by author shalashaska117 opened on Sep 25, 2026

• Z3 translation gives false refutations for rational and real Euclidean division

  vprover/vampire#994 · Filter by author shalashaska117 opened on Sep 25, 2026

• Debug interpolation asserts when constructing NonspecificInferenceMany for INPUT

  vprover/vampire#993 · Filter by author shalashaska117 opened on Sep 25, 2026

• SMT-LIB match on a non-datatype value triggers a Debug assertion

  vprover/vampire#992 · Filter by author shalashaska117 opened on Sep 25, 2026

• TPTP parser rejects valid integer and rational literals with a leading plus

  vprover/vampire#991 · Filter by author shalashaska117 opened on Sep 25, 2026

• Two Deque unit tests leak their heap-allocated containers

  vprover/vampire#990 · Filter by author shalashaska117 opened on Sep 25, 2026

• SMT datatype parse errors leak allocations before registration

  vprover/vampire#989 · Filter by author shalashaska117 opened on Sep 25, 2026

• Signature cleanup does not release registered term algebras

  vprover/vampire#988 · Filter by author shalashaska117 opened on Sep 25, 2026

• TPTP parser leaks temporary type-declaration nodes

  vprover/vampire#987 · Filter by author shalashaska117 opened on Sep 25, 2026

• Problem leaks model-reconstruction records after a successful solve

  vprover/vampire#986 · Filter by author shalashaska117 opened on Sep 25, 2026

• Problem does not release its cached Property during cleanup

  vprover/vampire#985 · Filter by author shalashaska117 opened on Sep 25, 2026

• Formula::destroy deletes a labelled BoolTermFormula twice

  vprover/vampire#984 · Filter by author shalashaska117 opened on Sep 25, 2026

• Inference::destroy falls through to the wrong payload destructor

  vprover/vampire#983 · Filter by author shalashaska117 opened on Sep 25, 2026