Three translation defects in tptp_frontend.cpp caused spurious sat/unsat
verdicts (reported as SZS BUG against annotated status):
- Parenthesized negation bound the whole disjunction: ( ~ p | q ) parsed
as ~(p | q) instead of (~p) | q, flipping nearly every CNF/FOF clause.
Negate only the next unary unit, then resume precedence parsing via a
new parse_binary_rest helper.
- Quantifier bodies absorbed lower-precedence connectives: ! [X] : p(X) => g
parsed as ! [X] : (p(X) => g). TPTP quantifiers bind tighter than the
binary connectives, so parse the body at parse_expr(PREC_EQ).
- Mixed Int/Real equality coerced through an uninterpreted box function,
severing arithmetic semantics and yielding spurious models. Use the
arithmetic to_real/to_int conversions instead.
Add regression cases to src/test/tptp.cpp covering all three fixes.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
`qe-lite` could produce malformed formulas when expanding bounded
quantifiers under nested binders, leaving outer de Bruijn indices
unshifted after eliminating an inner quantifier (e.g., `(:var 1)`
escaping capture). This change fixes index normalization in that rewrite
path and adds a regression for the reported forall/exists arithmetic
case.
- **Rewrite correctness in bounded quantifier expansion**
- In `src/qe/lite/qe_lite_tactic.cpp`, after substituting bounded
variables in payload conjuncts, apply `inv_var_shifter(num_decls)` so
outer bound variables are reindexed relative to the removed binder.
- This preserves quantifier structure correctness when
`try_expand_bounded_quantifier` eliminates an inner quantifier.
- **Regression coverage for the reported pattern**
- In `src/test/smt_context.cpp`, add a focused quantified arithmetic
formula matching the bug shape:
- outer `forall (x, x4)`
- inner `exists (y)`
- mixed inequalities that trigger qe-lite bounded expansion
- Assert the formula is unsatisfiable, preventing reintroduction of
invalid index handling in this path.
```c++
inst = vs(p, subst_map.size(), subst_map.data());
shift(inst, num_decls, inst); // reindex outer de Bruijn vars after eliminating inner quantifier
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`batch_manager::set_unknown()` in the parallel SMT tactic changed
`m_state` to `is_unknown` but never notified backbone workers or the
core-minimizer worker waiting on `m_bb_cv` / `m_core_min_cv`. Those
threads blocked indefinitely, deadlocking `solve()` at `t.join()`.
### Root cause
```
(declare-fun a (Int) Bool)
(declare-fun b (Int) Bool)
(assert (distinct a b))
(check-sat-using psmt)
```
Every CDCL worker returns `l_undef` with reason `(incomplete (theory
array))`. The first worker calls `set_unknown()` (a soft verdict — other
workers may still find sat/unsat) and exits. Other CDCL workers exit
when `get_cube()` checks `m_state != is_running`. Meanwhile, backbone
workers and the core minimizer are already blocked in
`wait_for_backbone_job()` / `wait_for_core_min_job()`, both of which
condition-wait on CVs that `set_unknown()` never signals. Their
predicates check `m_state != is_running`, but a CV predicate only
re-evaluates on notification or spurious wakeup.
### Fix
- **`src/solver/parallel_tactical.cpp`** — `set_unknown()` now calls
`m_bb_cv.notify_all()` and `m_core_min_cv.notify_all()` after setting
the terminal state, so waiting helper threads observe the change and
exit via the existing `m_state != is_running` guard in their wait
predicates.
### Test
- **`src/test/psmt.cpp`** — new regression covering SAT, UNSAT, and the
theory-incomplete (deadlock) path using `(as-array f)` terms to
reproduce the exact array-theory incompleteness that triggers
`set_unknown()`.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
## Summary
Fix a use-after-free in `func_interp::compress()`.
When a function interpretation had previously grown large enough to
allocate `m_entry_table`, `compress()` could deallocate entries whose
result matched the else-case but leave the hash table intact. Later
`get_entry()` lookups could then return freed `func_entry*` values,
which showed up during model checking as a corrupted expression result
from `model_evaluator`.
## Root cause
`func_interp::compress()` compacted `m_entries` and freed removed
entries, but it did not rebuild or clear `m_entry_table`.
This left stale pointers in the lookup table whenever:
- the table had already been allocated on a larger interpretation, and
- compression removed some entries.
In the reported case, model evaluation rewrote `stack_s!1041` through
`BR_REWRITE1`, fetched a freed `func_entry` result from the stale table,
and then tripped an assertion in `expr::get_sort()` during quantifier
model checking.
## Fix
After compression removes entries, rebuild `m_entry_table` from the
surviving `m_entries`, or clear it when the surviving interpretation is
small.
## Regression coverage
Added a unit regression in `src/test/model_evaluator.cpp` that:
- creates a `func_interp` large enough to allocate `m_entry_table`,
- compresses away almost all entries,
- checks that removed keys no longer resolve, and
- checks that the surviving key still resolves to the correct result.
## Validation
- `../build/z3 ebso-115.smt2` previously hit an assertion in
`rewriter_def.h` / `ast.cpp`; after the fix it no longer asserts.
- `./test-z3 model_evaluator` passes with the new regression.
## Reproducer
I did not produce a smaller SMT2 benchmark in this change. The original
reproducer I used was `ebso-115.smt2`, and the new unit regression
directly exercises the stale-entry-table path in-process.
Co-authored-by: Can Cebeci <t-cancebeci@microsoft.com>
This tightens two historical `nlsat` regressions that were still
print-only.
Closes#9859.
In `tst_16`, the test already exercises the old `lws2380` shape, but it
only dumped the projected clause. On current `master`, both projection
paths still keep the `x7`-linked root constraints, so this change turns
that observation into an assertion and updates the stale comment to
describe the current invariant.
In `tst_22`, the test already computes whether the projected lemma is
falsified at the stored counterexample. It previously printed the result
and kept going. This change adds `ENSURE(!all_false)` so the test fails
if that historical unsoundness shape comes back.
Testing:
`cmake --build . --target test-z3 -j1`
`./test-z3 /seq nlsat`
Implemented the largest cube heuristic from Bromberger and Weidenbach's
paper on cubes. Also fixes an overflow bug in mzp.
Use vswhere to find the visual studio version on windows in the build's ymls.
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
ZIPT review identified two hot-path inefficiencies in `euf_sgraph`:
`drop_left`/`drop_right` were implemented as repeated single-token drops
(`O(count × depth)`), and `classify` performed redundant string checks.
This change aligns behavior with the intended tree-navigation approach
while keeping semantics unchanged.
- **Algorithmic update: `drop_left` / `drop_right`**
- Replaced iterative `drop_first`/`drop_last` loops with direct
recursion over concat children.
- New logic drops across subtree boundaries using child lengths,
reducing work to tree depth (`O(depth)`).
- **Classification cleanup: `classify`**
- Collapsed double `is_string` probing into a single `is_string(e, s)`
call.
- Preserves existing kind mapping (`empty` vs non-empty string constant
handling).
- **Focused test coverage extension**
- Added boundary checks in `test_sgraph_drop` for `drop_left(..., 1)`
and `drop_right(..., 1)` on a 4-token concat tree.
```cpp
snode* sgraph::drop_left(snode* n, unsigned count) {
if (count == 0 || n->is_empty()) return n;
if (count >= n->length()) return mk_empty_seq(n->get_sort());
SASSERT(n->is_concat());
unsigned left_len = n->arg(0)->length();
if (count < left_len)
return mk_concat(drop_left(n->arg(0), count), n->arg(1));
return drop_left(n->arg(1), count - left_len);
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`seq_plugin::edit_distance_with_updates` used the left-string DP index
when checking whether the right string could accept an insertion from
the `d[i][j - 1]` transition. This miscomputed updateable edit distance
and could suppress valid repair proposals when `i != j`.
- **Bug fix**
- Change the right-side insertion guard in
`src/ast/sls/sls_seq_plugin.cpp` from `b.can_add(i - 1)` to `b.can_add(j
- 1)`.
- This aligns the mutability check with the DP transition being
evaluated and with the existing update-generation logic below it.
- **Regression coverage**
- Add a focused test in `src/test/sls_seq_plugin.cpp` for an asymmetric
variable/value layout on the right-hand side.
- The test asserts that the repair logic admits the right-side add at `j
- 1`, which is the case that the previous index mixup could reject.
- **Reference**
- The updated condition now matches the intended transition semantics:
```cpp
if (d[i][j - 1] < u[i][j] && b.can_add(j - 1)) {
m_string_updates.reset();
u[i][j] = d[i][j - 1];
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`euf_seq_plugin` was applying several regex concat simplifications
against raw child enodes instead of canonical e-graph roots, so rules
could silently miss after merges. It also merged loop bounds with
unchecked unsigned addition, allowing overflowed bounds.
- **Root-canonical checks in simplification rules**
- Use `get_root()` for nullable/full-seq absorption checks.
- Update `same_star_body` to test `is_star` on roots and compare rooted
star bodies.
- Evaluate extended star rules (`v*.v*.c` / `c.v*.v*`) against concat
roots, not syntactic children.
- **Safe loop merge arithmetic**
- Gate loop merging on overflow-safe bound addition checks before
constructing merged `re.loop`.
- **Re-simplify concats affected by child merges**
- In `propagate_merge`, re-run `propagate_simplify` for tracked concat
nodes whose left/right child root is in the merged class, not only
concats in the class itself.
- **Regression coverage in `src/test/euf_seq_plugin.cpp`**
- Added focused tests for:
- star merge firing after child-to-star merge,
- extended star rule using root concat shape,
- nullable absorption via merged roots,
- loop-merge non-application on overflow.
```cpp
// before: structural check on non-canonical enode
if (is_concat(b, b1, b2) && same_star_body(a, b1))
// after: structural check on canonical representative
if (is_concat(b->get_root(), b1, b2) && same_star_body(a, b1))
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Two fixes for mbp_dt_tg::apply() when encountering an accessor whose
argument has a different constructor in the model:
1. Don't call rm_accessor (which would assert a contradictory
recognizer, making the formula false). This prevents the original bug
where QEL returned 'false' for satisfiable formulas.
2. Branch on the model-assigned constructor for the accessor's argument.
The correct output should include the literal introduced in (2).
However, this fix does not produce it. Spacer is sound with this
over-approximation, as long as the counter example does not depend on
value of mismatched accessors (e.g. (tl nil)).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This change wires SMT-LIB Hilbert choice parsing to a concrete
array-theory operator and ensures both array backends enforce the
expected semantic axiom. Previously, `(choice ((x T)) phi)` parsed as
NYI and had no solver-side instantiation path.
- **Parser: lower `choice_k` into array `OP_CHOICE`**
- `pop_quant_frame(choice_k)` now builds `(choice p)` instead of
throwing.
- Added parser include/use of array utilities to construct the term
directly from the generated lambda predicate.
- **Array decl plugin: add `OP_CHOICE` typing + surface syntax**
- Added declaration support for `choice` with signature:
- `(Array T Bool) -> T` (encoded as `('a -> Bool) -> 'a` in HO view).
- Added recognizer/util helpers (`is_choice`, `mk_choice`) and exposed
`"choice"` in op names.
- **SMT array theory (`theory_array_full`): instantiate choice axiom**
- Added instantiation for each encountered `choice(p)`:
- `forall x . p(x) => p(choice(p))`
- Integrated into internalization/relevancy paths and statistics.
- **SAT/SMT array backend (`sat/smt/array_*`): instantiate choice
axiom**
- Added new axiom record kind for choice, internalization hook,
assertion routine, and diagnostics/stat tracking.
- Uses the same quantified implication schema as above.
- **Regression coverage**
- Extended SMT2 parser regression with an HO `choice` example to ensure
parser/eval pipeline accepts and processes choice terms.
Example of the now-supported input:
```smt2
(set-logic HO_ALL)
(declare-sort U 0)
(declare-fun P () (-> U Bool))
(assert (exists ((x U)) (P x)))
(assert (= witness (choice ((x U)) (P x))))
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
So far, `algebraic_numbers compare_core ` handles an edge case
incorrectly:
- If the two compared numbers (`a`, `b`) are different,
- the intervals still overlap after refinements, and
- both a and b are a root of the second polynomial (`cell_b->m_p`), e.g.
they are the first and second root
then the method would return `sign_zero` (i.e. "equal"). This behavior
can be replicated with the provided test case (before the fix). This
requires `algebraic.factor=false`, though i first encountered it during
solver runs on QF_NRA instances with the default
`algebraic.factor=true`, which apparently means that the polynomials for
anums are still not always factored.
The fix is to compare the interval bounds of b to a and vice versa. Then
the Sturm-Tarski check is only run if `a` and `b` both lie in the
intersection of the intervals, because only then is it guaranteed to be
correct.
The SMT2 front-end rejected valid higher-order inputs using `HO_ALL` and
failed on curried applications where the function position is itself an
expression (e.g., `((transfer top) 0)`).
This update adds `HO_ALL` support and makes curried parsing consistently
lower to implicit `select` chains.
- **Logic recognition**
- Treat `HO_ALL` as an `ALL`-class logic in SMT logic classification.
- This unblocks `(set-logic HO_ALL)` in the standard SMT2 command path.
- **Curried application parsing**
- Extend application-frame handling to support parenthesized expression
heads, not only symbol heads.
- When the head is an expression, parse application arguments normally
and construct nested implicit selects:
- `(f a b)` → `(select (select f a) b)`
- Preserve existing behavior for symbol-based applications, qualified
identifiers, and lambda-led forms.
- **Regression coverage**
- Add a focused parser/eval regression using the reported higher-order
case to lock in behavior.
```smt2
(set-logic HO_ALL)
(declare-fun transfer () (-> (-> Int Bool) (-> Int Bool)))
(assert (forall ((P (-> Int Bool))) (=> (P 0) ((transfer P) 0))))
(declare-fun top () (-> Int Bool))
(assert (forall ((x Int)) (top x)))
(assert (not ((transfer top) 0)))
(check-sat)
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Z3 could return `sat` for an unsatisfiable QF_ABV formula equating two
store chains over distinct constant arrays. The rewrite path for array
equalities was missing a necessary base-value constraint in
finite-domain cases where stores cannot cover all indices.
- **Root cause**
- In `array_rewriter::mk_eq_core`, equality rewriting for nested stores
over const-array bases did not enforce equality of the underlying const
values when the index domain size exceeds the number of updated indices.
- **Rewriter fix**
- Added a sound rewrite branch for:
- `store* ((as const ...) v)` vs `store* ((as const ...) w)`
- When `|domain| > (#stores_lhs + #stores_rhs)`, rewrite now includes:
- select equalities for touched indices (existing behavior)
- **and** base-value equality `v = w` (new requirement)
- This prevents spurious models where only updated indices are
constrained.
- **Regression coverage**
- Added a focused regression in `src/test/mod_factor.cpp` that asserts
`unsat` for a minimized constant-array/store-chain BV case with
`(distinct x y)` and one store per side.
```cpp
(assert (distinct x y))
(assert (= (store A0 i0 e0) (store A1 i1 e1)))
(check-sat) ; expected: unsat
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Fix the TPTP frontend so that a bare name used in an equality refers to
a single shared `func_decl`, regardless of how the surrounding context
coerces its sort.
## Problem
With the following input the conjecture was not proved:
```tptp
fof(a1,axiom, ! [X] : (X = a)).
fof(c1,conjecture, b = a).
```
`parse_atomic_formula` created bare names as 0-arity **Bool
predicates**, and `coerce_eq` later retyped them by calling
`m.mk_func_decl(...)` directly, without registering the result in
`m_decls`. So the `a` used inside `! [X] : (X = a)` (coerced to sort
`U`) and the `a` used inside `b = a` (left as Bool) ended up as two
unrelated `func_decl`s sharing only the name. The axiom no longer
constrained the conjecture.
## Fix
In `src/cmd_context/tptp_frontend.cpp`:
1. Add `mk_zero_arity_decl(name, range)` / `coerce_zero_arity(app*,
range)` helpers that memoize the 0-arity `func_decl` per `(name, target
sort)` in `m_decls`, delegating to the existing `mk_decl_or_ho_const`
for `U` and Bool targets.
2. Rewrite `coerce_eq` to use the new helpers and add an explicit Bool /
non-Bool retyping branch so a bare-Bool side is recast to the other
side's sort.
3. In `parse_atomic_formula`, when a bare name is immediately followed
by `=` or `!=`, create it as a non-predicate (sort `U`). Terms in
equalities are no longer first introduced as Bool predicates.
4. Reorder the constructor init-list so `m_univ` is initialized before
the pinned ref vectors (matches declaration order; silences
`-Wreorder`).
Net effect: every reference to a given name at a given sort yields the
same `func_decl`, eliminating duplicate-symbol bugs in equalities over
bare TPTP constants.
## Test
Added `fof-bare-constant-equality` to `src/test/tptp.cpp`. Without the
C++ change the new case asserts; with it, `./build/release/test-z3 /seq
tptp` reports `PASS`.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Spacer can crash on small HORN/ADT benchmarks when model construction
reaches datatype enodes without a fully populated constructor state. The
failure manifested as a null/invalid-path dereference inside datatype
model value generation.
- **Root cause area: datatype model extraction path**
- Hardened `theory_datatype::mk_value` to handle incomplete theory state
safely instead of assuming constructor metadata is always present.
- Added guarded fallback to a factory-provided datatype value when:
- `th_var` is missing,
- union-find lookup is invalid,
- var data/constructor is unavailable.
- **Behavioral change**
- Missing constructor state now degrades to a safe model value
(`expr_wrapper_proc`) instead of crashing during model generation.
- **Regression coverage**
- Added a focused API regression in `src/test/api_datalog.cpp` using a
Spacer + ADT HORN script (with reproducing seed) to ensure the code path
executes without parser/runtime failure.
```cpp
// theory_datatype::mk_value fallback shape
if (v == null_theory_var || invalid_var_data || d->m_constructor == nullptr) {
app* val = to_app(m_factory->get_some_value(n->get_sort()));
return alloc(expr_wrapper_proc, val);
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
