mirror of
https://github.com/Z3Prover/z3
synced 2026-06-23 09:00:30 +00:00
881360db5a
Z3 incorrectly returns SAT for formulas like `store(store(const(x), i0,
e0), i1, e1) = store(store(const(y), i0, e0), i1, e1) ∧ x ≠ y` when the
index sort has a small finite domain (e.g. `(_ BitVec 2)` = 4 elements).
The quantifier-based encoding of the same constraint correctly returns
UNSAT.
## Changes
### `src/sat/smt/array_solver.cpp` — `add_parent_lambda()`
When a store is added to an array's `m_parent_lambdas` after that array
already has `m_has_default = true` (i.e., a `default(array)` term
already exists in the e-graph), the default axiom for the new store was
silently dropped. This breaks the propagation chain:
```
default(const(x)) = x
↓ [via store default axiom]
default(store(const(x), i, v)) = x
↓ [via store default axiom]
default(store(store(const(x), ...), ...)) = x
↓ [EUF congruence from store equality]
x = y → contradiction
```
Fix: push `default_axiom(lambda)` in `add_parent_lambda` when
`m_has_default` is already set, so late-arriving stores still get their
default axioms instantiated.
```cpp
void solver::add_parent_lambda(theory_var v_child, euf::enode* lambda) {
auto& d = get_var_data(find(v_child));
ctx.push_vec(d.m_parent_lambdas, lambda);
if (should_prop_upward(d))
propagate_select_axioms(d, lambda);
if (d.m_has_default) // new: fire default axiom retroactively
push_axiom(default_axiom(lambda));
}
```
### Known remaining gap
`mk_eq_core` in `array_rewriter.cpp` also has a related issue: the
unconditional store-chain expansion fires only when `domain_size >
num_lhs + num_rhs` (line 893), but the correct threshold is `domain_size
> max(num_lhs, num_rhs)`. With 4-element domain and 2 stores per side,
`2+2 = 4` equals the domain size so the expansion is skipped. The
variant gated by `m_expand_store_eq` already uses `max()` correctly
(line 911); the unconditional path needs the same fix.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
|
||
|---|---|---|
| .. | ||
| sat_solver | ||
| smt | ||
| tactic | ||
| CMakeLists.txt | ||
| dimacs.cpp | ||
| dimacs.h | ||
| sat_aig_finder.cpp | ||
| sat_aig_finder.h | ||
| sat_allocator.h | ||
| sat_anf_simplifier.cpp | ||
| sat_anf_simplifier.h | ||
| sat_asymm_branch.cpp | ||
| sat_asymm_branch.h | ||
| sat_asymm_branch_params.pyg | ||
| sat_bcd.cpp | ||
| sat_bcd.h | ||
| sat_big.cpp | ||
| sat_big.h | ||
| sat_clause.cpp | ||
| sat_clause.h | ||
| sat_clause_set.cpp | ||
| sat_clause_set.h | ||
| sat_clause_use_list.cpp | ||
| sat_clause_use_list.h | ||
| sat_cleaner.cpp | ||
| sat_cleaner.h | ||
| sat_config.cpp | ||
| sat_config.h | ||
| sat_ddfw_wrapper.cpp | ||
| sat_ddfw_wrapper.h | ||
| sat_drat.cpp | ||
| sat_drat.h | ||
| sat_elim_eqs.cpp | ||
| sat_elim_eqs.h | ||
| sat_extension.h | ||
| sat_gc.cpp | ||
| sat_integrity_checker.cpp | ||
| sat_integrity_checker.h | ||
| sat_justification.h | ||
| sat_local_search.cpp | ||
| sat_local_search.h | ||
| sat_lookahead.cpp | ||
| sat_lookahead.h | ||
| sat_model_converter.cpp | ||
| sat_model_converter.h | ||
| sat_mus.cpp | ||
| sat_mus.h | ||
| sat_npn3_finder.cpp | ||
| sat_npn3_finder.h | ||
| sat_parallel.cpp | ||
| sat_parallel.h | ||
| sat_prob.cpp | ||
| sat_prob.h | ||
| sat_probing.cpp | ||
| sat_probing.h | ||
| sat_proof_trim.cpp | ||
| sat_proof_trim.h | ||
| sat_scc.cpp | ||
| sat_scc.h | ||
| sat_scc_params.pyg | ||
| sat_simplifier.cpp | ||
| sat_simplifier.h | ||
| sat_simplifier_params.pyg | ||
| sat_solver.cpp | ||
| sat_solver.h | ||
| sat_solver_core.h | ||
| sat_types.h | ||
| sat_watched.cpp | ||
| sat_watched.h | ||
| sat_xor_finder.cpp | ||
| sat_xor_finder.h | ||