check() now records the dependencies of an unsat subset in m_core, exposed via
ptr_vector<u_dependency> const& core(). On l_false it calls minimize_core:
with the new m_min_core flag (set_min_core, default true) it deletion-minimizes
to a minimal unsat subset containing only constraints that participate in the
contradiction; with the flag off it returns all membership dependencies.
Add unit tests asserting the core omits irrelevant constraints (e.g. x in a*,
x in ~a*, y in b* has core {x-constraints} only), exercising both flag states.
The test harness runs with minimization disabled by default.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Replace the batch solve_and(mems) with an incremental interface:
void add(expr* term, expr* regex, u_dependency* d);
lbool check();
add() stores each (term, regex, dependency) triple in
m_memberships (vector<tuple<expr_ref, expr_ref, u_dependency*>>); the
dependency is retained for future unsat-core tracking and may be nullptr.
check() decides the accumulated conjunction (the former solve_and body) and
consumes the memberships; an empty conjunction is sat. Update the unit tests
and benchmark to the add()/check() API.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Remove the obj_map<expr,expr*>* model out-parameter from solve/solve_and/
decide_dnf. Add an m_gen_model flag (default true) with set_gen_model(bool),
store the extracted model in m_model (reset at the top of decide_dnf), and
expose get_model(). Switch live_states out to expr_ref_vector and the
product_nonempty state vectors to ptr_vector<expr>. Simplify the concat case
of parse_term with all_of. Disable model generation in the sat-only unit
tests and the benchmark.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
Per-variable extra constraints are now expressed as additional (var in R')
memberships passed to solve_and, so the var_extra parameter is dropped from
solve/solve_and and the internal decide_dnf. Tests updated to route extra
constraints through solve_and.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
## Summary
Register the opt-in seq_monadic benchmark harness in test-z3.
The harness reads either Z3_SEQ_BENCH_FILE or all SMT2 files under
Z3_SEQ_BENCH_DIR, supports Brz and light-Ant modes through
Z3_SEQ_MONADIC_MODE, and reports per-file CSV timing and verdict
information.
Light-weight Antimirov cofactors for seq_monadic
================================================
Overview
--------
The seq_monadic solver explores symbolic regex derivatives when
computing live
states and product transitions. Its original transition representation
used
Brzozowski cofactors.
This change adds a light-weight Antimirov representation. It first
computes the
existing Brzozowski cofactors and then decomposes targets whose outer
shape is
s1 | ... | sn
or
(s1 | ... | sn) . tail
into separate transitions. Concatenations are maintained in
right-associative
form, so a distributable union occurs as the head of the concatenation.
Targets are reconstructed with mk_regex_concat to preserve
normalization.
After decomposition, transitions with the same target are merged by
disjoining
their guards. The existing path-aware cofactor traversal and range
predicates
are therefore retained.
Example
-------
For
r = .* a .{k}
the Brzozowski cofactors have the shape
[a, r | .{k}]
[^a, r]
The light-weight Antimirov transformation produces
[., r]
[a, .{k}]
This preserves the language while avoiding the deterministic subset
states
that grow exponentially on this family.
Modes
-----
seq_monadic exposes two transition modes:
light_antimirov default
brzozowski retained as an explicit option
The implementation is seq_rewriter::light_ant_derivative_cofactors.
Correctness
-----------
The seq_monadic unit tests run in both modes. They cover character and
generic
element sequences, multiple and repeated variables, variable
constraints,
bounded loops, conjunctions of memberships, and witness construction. A
focused test checks the cofactor transformation above. The complete
94-test
unit suite used during evaluation passed. The benchmark harness is not
registered as a normal unit test; after detaching it, all 93 registered
tests
pass.
Benchmark evaluation
--------------------
The final optimized comparison used all 1,545 SMT2 files under
C:\git\bench\inputs\regexes. Each file was run in a separate process
with a
15-second timeout. There were 1,513 cases where both modes completed
without a
process failure or timeout.
Brzozowski Light-Ant
paired solver time 94.98 s 63.26 s
median solver time 1.734 ms 0.710 ms
derivative calls 5.70 M 3.39 M
cofactors 13.33 M 6.99 M
live states 2.74 M 0.44 M
product states 652.8 K 642.8 K
Light-Ant reduced paired solver time by 33.4%, derivative calls by
40.5%,
cofactors by 47.5%, and live states by 84.0%. It was faster on 1,091
cases;
Brzozowski was faster on 421 cases.
Light-Ant changed 131 Brzozowski undef results to sat. There were no
reverse
verdict changes and no mismatches against known sat/unsat statuses. Both
modes
had two timeouts. Process failures decreased from 30 to 27.
By corpus, paired solver time improved by 39.1% on ClemensRegex and by
11.9% on
MargusRegex.
Alternatives considered
-----------------------
Direct use of full Antimirov derivatives was also evaluated. It
introduced
large performance outliers, particularly around intersections, and
produced
additional undef results and timeouts. Disabling intersection-over-union
distribution improved some of these cases but remained slower and less
robust
than the light-weight transformation. The direct full-Ant mode was
therefore
removed from this change.
Copilot-Session: a2ce3573-4e15-4a4a-afb5-21e3cb04e4a2
Remove the seq_split (regex sigma-splitting / factorization) module and all
code that uses it:
- delete src/ast/rewriter/seq_split.{h,cpp} and src/test/seq_split.cpp
- drop the m_split member, include, and split/simplify_split/split_membership
wrappers from seq_rewriter
- remove the regex factorization propagation block from seq_regex.cpp
- remove the seq.regex_factorization_enabled/threshold parameters and their
theory_seq_params fields
- drop the files from the rewriter/test CMake lists and the test registry
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 57b9b87e-950a-49ea-bbb3-ed585646a5a9
## Summary
Adds `seq_monadic` (`src/ast/rewriter/seq_monadic.{h,cpp}`), a
self-contained,
rewriter-level decision procedure for regex membership of a term that is
a
concatenation of sequence variables and constant elements — e.g. `x·a·x
∈ R`,
including repeated and multiple variables. It uses a whole-language
*monadic
decomposition* plus automaton product-reachability; it is minterm-free
and does
**not** use Nielsen word-equation splitting or `seq_split`.
The component is **purely additive**: it is not wired into any solver
path, so
default behavior is unchanged. It ships with a unit test and an opt-in
benchmark
harness that is inert unless `Z3_SEQ_BENCH_DIR` is set.
## What it does
- `x·u ∈ R ⇔ ⋁_q ( x reaches q in A_R ∧ u ∈ q )` over the derivative
automaton; `reach(q)` is never materialized as a regex (avoids the
state-elimination blowup). A variable's constraint is decided by a lazy
product-reachability search over tuples of derivative states, with
transitions
= the product of `brz_derivative_cofactors` branches and
pairwise-conjoined
`seq::range_predicate` guards.
- **Generic in the element sort**: characters use the exact
`range_predicate`
algebra; any other element sort uses a candidate-basis over the element
values
the guards mention (sound and complete for the
`{true,false,=,<=,and,or,not}`
guard grammar the derivatives emit).
- **Concrete witnesses**: on sat it reconstructs a witness value (a
sequence of
concrete elements, not predicates) per variable from the accepting
product path.
- **Boolean combinations**: `solve_and` decides a conjunction of
memberships
jointly, so a variable shared across memberships is constrained
consistently.
This is the natural extension since `¬(t∈R) ≡ t∈~R`, `∨` = union of
DNFs, and
`∧` = product of DNFs.
Also de-duplicates the char-guard → `range_predicate` translator into a
single
public `seq::guard_to_range_predicate` in `seq_range_collapse` (it was
previously
duplicated there and in `seq_monadic`).
## Testing
- `tst_seq_monadic`: single / multiple / repeated variables, nested
complement,
bounded loops, per-variable constraints, a generic `(Seq Int)` section,
witness
verification (substitute the model back and re-decide membership), and
`solve_and` cases that are individually sat but jointly unsat.
- Full unit suite `test-z3 /a` passes (93/93).
## Evaluation (offline harness, not part of CI)
On a regex-membership benchmark corpus, restricted to files carrying a
genuine
`(set-info :status)`, the solver decides 318 and 316 are correct
(99.4%); the
only 2 disagreements are a length limitation (`|x|=2k`) that is outside
the
membership fragment.
## Known limitations / follow-ups
- Pathological deeply-nested, high-multiplicity regexes can overflow the
recursive derivative stack; a recursion-depth guard to degrade to
`unknown` is
a natural follow-up.
- Out-of-fragment constraints (word equations, length / Parikh) are not
handled,
by design — this decides regex membership only.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Copilot-Session: 916db256-43c6-4067-b6f4-fa8d2cf2f37f
`scanner::scan()` was returning `EOF_TOKEN` when the underlying stream
had `badbit` set, making a failed read (EIO, ENOSPC, etc.)
indistinguishable from a clean end-of-file. Z3 would silently produce no
output with exit code 0.
## Root cause
`std::istream::gcount()` returns 0 for both normal EOF and I/O failure.
`read_char()` returned -1 in both cases, and `scan()`'s `-1` handler
unconditionally set `EOF_TOKEN`.
## Fix
### `src/parsers/util/scanner.cpp`
Check `m_stream.bad()` in the `-1` case; emit an error message and
`ERROR_TOKEN` on failure:
```cpp
case static_cast<char>(-1):
if (m_stream.bad()) {
m_err << "ERROR: I/O failure while reading input stream.\n";
m_state = ERROR_TOKEN;
} else {
m_state = EOF_TOKEN;
}
break;
```
### `src/test/scanner_io.cpp` (new)
Regression test (ported from the `io_test` branch) verifying:
1. A good stream scans to completion (`n > 0` tokens).
2. A stream with `badbit` pre-set produces `ERROR_TOKEN` or a non-empty
error message rather than silent EOF.
### `src/test/main.cpp` + `src/test/CMakeLists.txt`
Register `tst_scanner_io` in the `FOR_EACH_ALL_TEST` macro and add
`scanner_io.cpp` to the build.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
Expose enum_tuples(sorts) which produces an iterator over vectors of
terms, one term per input sort, dovetailing the per-sort streams so all
combinations are enumerated even when individual streams are infinite.
Each sort is enumerated by a self-contained sort_stream owning its own
grammar and bottom_up_enumerator seeded from the user productions, so
array sorts (with their fresh select ops and bound vars) do not collide
across sorts.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: cb1e958b-f89b-4407-958d-8e7ecf172bbc
`memory_max_size` OOMs were recoverable at `check_sat` time
(`Z3_L_UNDEF` + error handler), but `Z3_solver_reset` could still
terminate the process with an uncaught `out_of_memory_error`. This
change keeps reset on the C API error-reporting path instead of letting
teardown allocations trip the same hard limit.
- **Reset path hardening**
- `Z3_solver_reset` now performs solver teardown under a temporary
suspension of the global memory cap, then restores the previous cap
afterward.
- This avoids aborts when allocator accounting is still above
`memory_max_size` at reset time.
- **Memory manager support**
- Added `memory::get_max_size()` to snapshot/restore the active cap
precisely.
- **Regression coverage**
- Extended `src/test/memory.cpp` with a focused scenario that trips
`Z3_MEMOUT_FAIL` and then calls `Z3_solver_reset` under a non-throwing
error handler, covering the previously aborting recovery path.
```cpp
struct scoped_memory_limit_reset {
size_t m_prev_max;
scoped_memory_limit_reset(): m_prev_max(memory::get_max_size()) {
memory::set_max_size(0);
}
~scoped_memory_limit_reset() {
memory::set_max_size(m_prev_max);
}
} scoped_max_memory;
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10250
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`euf-completion` crashed with an assertion violation on any unary
negation of a nonlinear product (e.g. `(= (- (* a a)) a)`), because
`register_node` hit `NOT_IMPLEMENTED_YET()` in the `is_uminus` branch.
## Changes
- **`src/ast/euf/euf_arith_plugin.cpp`**: Replace
`NOT_IMPLEMENTED_YET()` with the natural rewrite `-x ↦ (-1) * x`,
consistent with how subtraction is already handled (`x - y ↦ x + (-1 *
y)`). Creates the `-1` numeral of the correct sort, builds the
multiplication enode, and merges via `push_merge`.
- **`src/test/euf_arith_plugin.cpp`**: Add `test4` exercising the exact
repro shape — negation of a nonlinear product merged with a variable.
```smt2
(declare-const a Real)
(set-simplifier euf-completion)
(assert (= (- (* a a)) a))
(check-sat) ; previously: ASSERTION VIOLATION — now: sat
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10240
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
MinGW silently ignores `#pragma comment(lib, ...)` (MSVC-only), so
linker errors like missing `dbghelp` symbols go undetected until a
downstream user hits them. No CI coverage existed for MinGW on Windows.
## Changes
- **`.github/workflows/Windows.yml`**: New `mingw-build` job using MSYS2
UCRT64 (`mingw-w64-ucrt-x86_64-gcc`) that builds Z3 via `cmake -G Ninja`
and runs `test-z3 /a`, exercising the full link step under MinGW on
every push/PR to master.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `Ubuntu build - python make - MT` job was failing in unit test
`max_reg` under debug configuration due to a shape-sensitive internal
NLA assertion. This PR updates the test’s nonlinear expressions to an
equivalent construction that avoids the failing path.
- **Root issue in CI path**
- `test_max_reg` built BNH objective/constraints with subtraction forms
that triggered a debug-only monic-check assertion in NLA internals.
- **Targeted test-only normalization**
- In `src/test/api.cpp` (`test_max_reg`), rewrote squared-difference
terms to constant-first subtraction forms (mathematically equivalent).
- Updated:
- `f2` construction
- circle/offset constraints in `mk_max_reg()`
- **No solver behavior change**
- This is a unit-test expression-shape change only; production solver
code is untouched.
```cpp
// before
Z3_ast f2 = mk_add(mk_sq(mk_sub(x1, mk_real(5))), mk_sq(mk_sub(x2, mk_real(5))));
Z3_optimize_assert(ctx, opt, Z3_mk_le(ctx,
mk_add(mk_sq(mk_sub(x1, mk_real(5))), mk_sq(x2)), mk_real(25)));
// after
Z3_ast f2 = mk_add(mk_sq(mk_sub(mk_real(5), x2)), mk_sq(mk_sub(mk_real(5), x1)));
Z3_optimize_assert(ctx, opt, Z3_mk_le(ctx,
mk_add(mk_sq(mk_sub(mk_real(5), x1)), mk_sq(x2)), mk_real(25)));
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
With `(set-option :smtlib2_compliant true)`, Z3 disables implicit
Int→Real coercions. When the LP solver generates Gomory cuts/bounds over
expressions that mix Int and Real LP variables (as happens when
`to_real(n)` is internalized — both `to_real(n)` as Real and `n` as Int
are registered as LP vars), `coeffs2app` was constructing
`mk_mul(Real_numeral, Int_expr)`. Without implicit coercions,
`check_args` throws an `ast_exception` that bubbles up through
`cmd_context::check_sat()` as `l_undef`, producing a spurious `unknown`
instead of `unsat`.
## Changes
- **`src/smt/theory_lra.cpp` — `coeffs2app`**: Before building each
product term, coerce `o` to Real via `a.mk_to_real(o)` when `!is_int &&
a.is_int(o)`. This makes the sort explicit rather than relying on
implicit coercions.
- **`src/test/smt2print_parse.cpp`**: Regression test for the exact
formula from the issue — verifies the result is `unsat` (not `unknown`)
when `smtlib2_compliant` is set.
```smt2
(set-option :smtlib2_compliant true)
(set-logic ALL)
(declare-datatype SBVRational ((SBV.Rational (sbv.rat.numerator Int) (sbv.rat.denominator Int))))
; ... mixed Int/Real via to_real ...
(check-sat)
; was: unknown (:reason-unknown "Sort mismatch at argument #2 for function * (Real Real) Real supplied sort is Int")
; now: unsat
```
<!-- START COPILOT CODING AGENT SUFFIX -->
- Fixes#10166
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
These tests fed a fixed SMTLIB2 string to Z3_eval_smtlib2_string and checked
a sat/unsat verdict. They are now data-driven regression files under
z3test regressions/smt2 (with .expected.out ground truth), so remove them
from the C++ test suite:
- fpa.cpp: removed entirely (all tests transferred)
- seq_rewriter.cpp: removed the two seq.foldl model-validation tests
- simplifier.cpp: removed the sat.smt QF_UFBV predicate model-validation test
- mod_factor.cpp: removed the const-array store-chain unsat test
The API-constructed mod/idiv internalization-order tests remain in mod_factor.cpp.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
## Summary
Include the equal-width case in symbolic unsigned BV-to-FP exponent
saturation,
preventing positive exponents from being interpreted as negative by the
rounder.
Adds regression coverage for overflow and in-range values.
Fixes#7135.
## Testing
- `./build-review/test-z3 fpa`
- `./build-review/test-z3 /a` (92 passed)
- Symbolic-versus-numeral differential matrix (50 cases across five
width boundaries and all rounding modes)
- Exact-head fork `CI` and `OCaml Binding CI` workflows (passed)
Symbolic `re.range` nested under `re.++` caused Z3 to loop indefinitely,
ignoring timeouts. Direct symbolic range membership was fixed
previously, but the nested case reaches a different code path — the
Brzozowski derivative engine in `derive_range`.
## Root cause
`derive_range` in `seq_derive.cpp` only handled concrete unit-string
bounds. For symbolic bounds it returned a stuck `re.derivative(ele,
re.range(lo, hi))` term. When nested under concatenation, this stuck
term cycled infinitely:
1. `is_nullable` of the stuck term → `is_nullable_symbolic_regex` →
emits `re.in_re("", re.derivative(...))`
2. That `in_re` triggers `propagate_in_re` → new `accept` predicate
3. New `accept` computes another derivative → another stuck term →
repeat
## Fix
Replace the stuck fallback with a proper symbolic ITE. By SMT-LIB
semantics, `re.range(lo, hi)` accepts character `c` iff both bounds are
single-character strings and `lo[0] ≤ c ≤ hi[0]`. The derivative with
respect to `ele` becomes:
```
ite(len(lo)=1 ∧ len(hi)=1 ∧ lo[0] ≤ ele ∧ ele ≤ hi[0], ε, ∅)
```
Length conditions are omitted for bounds already known to be concrete
single-character strings.
```smt2
(set-logic ALL)
(declare-const s String)
(assert (str.in_re "a" (re.++ re.all (re.range s "c"))))
(check-sat)
; Previously hung indefinitely; now returns sat in ~10ms
```
## Changes
- **`src/ast/rewriter/seq_derive.cpp`** — `derive_range`: replace stuck
`re.derivative` fallback with symbolic ITE using `str.nth_i` and length
guards for non-concrete bounds
- **`src/test/seq_rewriter.cpp`** — add solver-level regression test
(case 21) for nested symbolic `re.range` under `re.++`
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Validate a polymorphic declaration's arity before matching argument
sorts. This prevents
`Z3_mk_app` from reading past the declaration domain and makes both
too-few and too-many
arguments return `Z3_INVALID_ARG`.
Adds C API regression coverage for valid, too-few, and too-many
applications.
Fixes#10177.
## Testing
- `./build-release/test-z3 api`
- `./build-release/test-z3 /a` (92 passed)
- Standalone #10177 reproducer against the patched shared library
Large Python bitvector workloads were hitting a sharp performance cliff
during `Solver.add(...)`, consistent with severe hash-table clustering
in expression-heavy assertion paths. The issue was sensitive to input
size/alignment, indicating weak low-bit dispersion in hash combination.
- **Hash mixing update (`src/util/hash.h`)**
- Replaced the old `combine_hash(h1, h2)` arithmetic/xor sequence with
stronger mixing:
- boost-style combine step
- `hash_u(...)` finalization
- Goal: improve low-bit entropy used by chained hash-table bucket
selection under aligned/high-volume AST patterns.
- **Regression guard and A/B comparison (`src/test/chashtable.cpp`)**
- Added `tst_combine_hash_low_bits()` and invoked it from
`tst_chashtable()`.
- The test stresses aligned first components (`i << 12`) combined with a
fixed seed.
- Added an in-test comparison between the **old** and **new** pairwise
hash combiners and validates:
- reduced collision counts for low-bit projections (8-bit and 16-bit
suffixes),
- improved low-bit uniformity for 8-bit and 16-bit suffixes,
- reported prefix/suffix uniformity metrics (high/low 8 and 16 bits) for
visibility in test output.
```cpp
static inline unsigned combine_hash(unsigned h1, unsigned h2) {
h1 ^= h2 + 0x9e3779b9 + (h1 << 6) + (h1 >> 2);
return hash_u(h1);
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`seq.foldl` could produce a concrete sequence model while related
`seq.nth` constraints were still validated against stale or
underconstrained length information, leading to invalid models. In the
reported case, `all` was modeled as `(seq.++ (seq.unit 7) (seq.unit 0))`
while `final = (seq.nth all 0)` remained inconsistent with `final = 6`.
- **Root cause**
- Sequence solutions were propagated as equalities, but parent `seq.len`
terms were not updated when a sequence term was solved.
- As a result, `seq.nth` guard reasoning could miss that a solved
sequence had known in-bounds length.
- **Solver change**
- Extend `theory_seq::add_solution` to collect parent `seq.len`
expressions of a solved term when the solved result is sequence-typed.
- After propagating the solved sequence equality, also propagate the
rewritten length equality for those parent length terms.
- Keep this propagation guarded to sequence results so scalar
`seq.foldl`/`seq.foldli` solutions do not regress from `sat` to
`unknown` under model validation.
- **Regression coverage**
- Add a focused test for the reported SMT-LIB pattern:
- `all = seq.foldl(...)`
- `final = seq.nth all 0`
- `initial = 0`
- `final = 6`
- Add focused scalar `seq.foldl`/`seq.foldli` model-validation coverage
for the existing benchmark shapes that must continue returning `sat`.
- The regressions check both that model validation no longer reports an
invalid model for the `seq.nth` case and that scalar fold/foldi cases do
not regress to `unknown`.
- **Effect**
- Solved sequence terms now push enough derived length information for
dependent `seq.nth` constraints to validate against the actual modeled
sequence.
- Existing scalar fold/foldi solving behavior is preserved.
```smt2
(define-fun all_sums ((prev_sums (Seq Int)) (elem Int)) (Seq Int)
(seq.++ (seq.unit (+ (seq.nth prev_sums 0) elem)) prev_sums)
)
(assert (= all (seq.foldl all_sums (seq.unit initial) elements)))
(assert (= final (seq.nth all 0)))
(assert (= initial 0))
(assert (= final 6))
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The reported case showed expensive reasoning for lexicographic string
comparisons under the default sequence solver, and incorrect handling
expectations with `z3str3` (which does not interpret these comparisons).
This change targets the default solver path by short-circuiting
contradictory constant-bound `<` constraints earlier.
- **Theory shortcut for constant lexical bounds**
- In `theory_seq::assign_eh`, detect asserted `str.<` constraints of the
form `c < x` or `x < c` where `c` is a string constant.
- When a complementary bound on the same equivalence class is already
true, check bound consistency immediately.
- If bounds are contradictory (`!(lower < upper)`), emit a direct theory
conflict from the two active literals instead of waiting for deeper
axiom propagation.
- **Preserve existing comparison reasoning**
- Existing `check_lts` transitivity/axiom flow is retained.
- The new logic is a narrow fast path for contradictory constant bounds
and does not alter general string-order semantics.
- **Regression coverage**
- Added a solver-level regression in `src/test/seq_rewriter.cpp` for
contradictory date-like lexical bounds to ensure this class of
constraints is rejected as `unsat`.
```cpp
ctx.assert_expr(su.str.mk_lex_lt(su.str.mk_string("2024-01-01"), x));
ctx.assert_expr(su.str.mk_lex_lt(x, su.str.mk_string("2024-12-31")));
ctx.assert_expr(su.str.mk_lex_lt(x, su.str.mk_string("2023-01-01")));
ENSURE(ctx.check() == l_false);
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Combining `mod0`/`div0` quantifier axioms with a mod-idempotency
quantifier caused Z3 to loop forever. The core issue was that
`mk_mod_core` in `arith_rewriter.cpp` only handled rewrite rules for
*numeral* moduli, leaving two gaps for symbolic `y`:
1. `mod(a + k*y, y)` was not reduced to `mod(a, y)`, so `(not (= (mod (+
a b) b) (mod a b)))` stayed unreduced and caused the nlsat solver to
spin.
2. The E-matching pattern `(mod (mod x y) y)` fired on every new term it
produced, creating an unbounded chain of nested `mod` expressions.
```lisp
; Previously non-terminating, now returns unsat immediately
(assert (forall ((x Int)) (! (= (mod0 x 0) 0) :pattern ((mod0 x 0)))))
(assert (forall ((x Int)) (! (= (div0 x 0) 0) :pattern ((div0 x 0)))))
(assert (forall ((x Int) (y Int))
(! (= (mod (mod x y) y) (mod x y)) :pattern ((mod (mod x y) y)))))
(assert (not (= (mod (+ a b) b) (mod a b))))
(check-sat)
```
## Changes
- **`src/ast/rewriter/arith_rewriter.cpp` — symbolic summand
elimination**: In `mk_mod_core`, when the modulus is a non-numeral
integer and the dividend is an `add`, strip any summand equal to the
modulus or an integer multiple of it. Soundness: `k*0 = 0` for all `k`,
so the rule holds even at `y = 0`. This immediately collapses the
reported formula to `false`.
- **`src/ast/rewriter/arith_rewriter.cpp` — symbolic idempotency via
ite**: Extend the existing `mod(mod(x,y), y) → mod(x,y)` rule
(previously numeral-only) to symbolic `y` by rewriting to `ite(y=0,
mod(mod(x,0),0), mod(x,y))`. The `y=0` branch uses a numeral divisor,
which is excluded by the `!v2.is_zero()` guard, halting the E-matching
chain.
- **`src/test/arith_rewriter.cpp`**: Regression tests for `mod(a+y, y) =
mod(a,y)`, `mod(a+2y, y) = mod(a,y)`, and `mod(mod(a,3),3) = mod(a,3)`.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `api_datalog` unit test was failing in CI with `"the logic has
already been set"`. Two consecutive regression tests shared a single
`Z3_context`, but both called `Z3_eval_smtlib2_string` with `(set-logic
HORN)` — the second call always fails because context logic state is
permanent.
## Changes
- **`src/test/api_datalog.cpp`**: Give each
`Z3_eval_smtlib2_string`-based regression test its own
`Z3_config`/`Z3_context`, destroyed immediately after the test block.
The outer context is retained only for the two tests that don't invoke
the SMT-LIB evaluator.
```cpp
// Before: both blocks shared `ctx`, second (set-logic HORN) always errored
Z3_string response = Z3_eval_smtlib2_string(ctx, chc1); // sets HORN logic
Z3_string response = Z3_eval_smtlib2_string(ctx, chc2); // ERROR: logic already set
// After: each block owns its context
Z3_config cfg2 = Z3_mk_config();
Z3_context ctx2 = Z3_mk_context(cfg2);
Z3_del_config(cfg2);
Z3_string response = Z3_eval_smtlib2_string(ctx2, chc2);
Z3_del_context(ctx2);
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`check-sat-using qe` was reported to return `unsat` on a satisfiable
quantified-real formula, while a subsequent `check-sat` on the same
assertion returned `sat`. This PR adds focused regression coverage for
that shape to prevent reintroduction.
- **Regression coverage for the reported formula**
- Added `test_qe_regression_4175()` in `src/test/quant_solve.cpp`.
- Parses and quantifier-eliminates:
```smt2
(forall ((b Real)) (= (= r1 b) (= b 0)))
```
- **Behavioral oracle encoded in the test**
- Verifies the QE result is satisfiable under `r1 = 0`.
- Verifies the QE result is unsatisfiable under `r1 != 0`.
- This captures the intended semantics of the original formula and
guards against the unsound `unsat` outcome from the QE path.
- **Integration**
- Wires the new regression into `tst_quant_solve()` so it runs with
existing quantifier-solver test coverage.
Example snippet from the new test logic:
```cpp
solver.assert_expr(result);
solver.assert_expr(m.mk_eq(r1, zero));
VERIFY(l_true == solver.check());
solver.assert_expr(result);
solver.assert_expr(m.mk_not(m.mk_eq(r1, zero)));
VERIFY(l_false == solver.check());
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Spacer crashed in quantifier-elimination projection on certain HORN
inputs when model evaluation produced arithmetic expressions that were
not plain numerals. The failure was an assertion in
`spacer_qe_project.cpp` during sign/offset computation for projected
literals.
- **Projection robustness in Spacer arithmetic QE**
- Updated numeral extraction in `src/muz/spacer/spacer_qe_project.cpp`
from `is_numeral` to `is_extended_numeral` at all model-evaluation sites
used by projection.
- This covers evaluated arithmetic forms (e.g., normalized arithmetic
expressions) that are semantically numeric but not syntactic numerals,
preventing assertion failures in disequality/equality handling and bound
selection.
- **Regression coverage for the crashing HORN shape**
- Added a focused regression in `src/test/api_datalog.cpp` that
evaluates the reported Spacer/HORN input pattern through
`Z3_eval_smtlib2_string`.
- The test exercises the exact QE/projection path that previously
triggered the assertion.
```cpp
// Before
VERIFY(a.is_numeral(val, r));
// After
VERIFY(a.is_extended_numeral(val, r));
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Unit tests relied on `SASSERT()` which is a no-op in release builds
(`DEBUG_CODE` wrapper), silently skipping all assertions outside debug
mode. Several test files were also gated behind `#ifdef _WINDOWS`,
making them dead code on Linux/macOS CI.
## Changes
- **`SASSERT` → `ENSURE` in 20 test files (200 occurrences)**: `ENSURE`
maps to `VERIFY` and always executes regardless of build type, ensuring
test assertions are active in both debug and release builds.
- **`src/test/diff_logic.cpp`**: Removed `#ifdef _WINDOWS` wrapping the
entire file. No Windows-specific APIs were used; the guard only
prevented compilation on non-Windows platforms.
- **`src/test/dl_product_relation.cpp`**: Removed `#ifdef _WINDOWS`
guard around `tst_dl_product_relation()`. The function body has no
platform dependencies.
- **`src/test/sat_local_search.cpp`**: Replaced `sscanf_s`
(MSVC-specific) with portable `sscanf`; added return-value check to
detect malformed input. Previously, `build_instance()` unconditionally
returned `false` on non-Windows, making the SAT local search test a
no-op on Linux/macOS.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Fixes a **soundness regression** in the sequence/regex rewriter: a
symbolic character range such as `(re.range x x)` was unsoundly
collapsed to `re.empty`, causing a satisfiable membership constraint to
be reported `unsat`.
This was surfaced by the `snapshot-regression` corpus in
`Z3Prover/bench`.
- **Originating discussion:**
https://github.com/Z3Prover/bench/discussions/2761
- **Benchmark:** `iss-5873/bug-2.smt2` (in `Z3Prover/bench`, under
`inputs/issues/iss-5873/`)
- **z3 under test at capture:** `z3-4.17.0-x64-glibc-2.39` (Nightly)
## Divergence
The recorded oracle expects `sat`; current z3 returns `unsat`:
```diff
--- bug-2.expected.out (expected)
+++ produced (current z3)
@@ -1,3 +1,4 @@
-sat
-((tmp_str0 "\u{0}"))
+unsat
+(error "line 12 column 10: check annotation that says sat")
+(error "line 14 column 22: model is not available")
(:reason-unknown "")
```
The benchmark asserts (simplified):
```smt2
(assert (= (str.in_re (str.replace tmp_str0 tmp_str0 tmp_str0)
(re.range tmp_str0 tmp_str0))
(str.contains tmp_str0 tmp_str0)))
```
`str.contains x x` is always true and `str.replace x x x = x`, so this
requires `str.in_re x (re.range x x)` to hold, which is satisfiable
exactly when `x` is a single character (`len(x) = 1`).
## Root cause
`seq_rewriter::mk_re_range` treated any bound that is not a concrete
single-character literal as making the whole range **empty**:
```cpp
if (str().is_string(lo, slo) && slo.length() == 1) clo = slo[0];
else if (str().is_unit(lo, lo1) && m_util.is_const_char(lo1, clo)) ;
else is_empty = true; // unsound for a symbolic bound
```
For a symbolic bound this is unsound: `(re.range x x)` denotes `{x}`
whenever `x` is a single character, not `∅`. Collapsing it to `re.empty`
makes `str.in_re x (re.range x x)` false, contradicting the (true)
`str.contains x x`, so the solver derives an unsound `unsat`.
`git blame` attributes this unsound collapse to z3 commit `15f33f458d`
("Derive with ranges (#9965)"), which post-dates the oracle capture.
## Fix
Two surgical changes in `src/ast/rewriter/seq_rewriter.cpp`:
1. **`mk_re_range`** no longer assumes emptiness for symbolic bounds. It
concludes `re.empty` only when it can *prove* emptiness — a bound whose
length can never be 1, or two concrete bounds with `lo > hi`. When a
bound is symbolic it returns `BR_FAILED` and keeps the range. Concrete
single-character ranges keep their existing handling (`lo == hi →
str.to_re`, inverted → `re.empty`).
2. **`mk_str_in_regexp`** reduces membership in a range that has a
symbolic bound to the equivalent length/order constraints, which are
sound and complete under SMT-LIB `re.range` semantics:
`str.in_re e (re.range lo hi)` ⟶ `len(lo)=1 ∧ len(hi)=1 ∧ len(e)=1 ∧ lo
≤ e ∧ e ≤ hi`
(using `str.<=`). The derivative engine only unfolds ranges whose bounds
are concrete characters, so without this reduction a symbolic-bound
range would otherwise be left unsolved.
## Validation
Rebuilt z3 from this branch on the workflow runner (`./configure && make
-C build -j$(nproc)`) and re-ran the failing benchmark with the same
option the snapshot capture uses (`-T:20`):
```
$ z3 -T:20 inputs/issues/iss-5873/bug-2.smt2
sat
((tmp_str0 "A"))
(:reason-unknown "")
```
The verdict is now **`sat`** (was `unsat`) — the soundness regression is
resolved. A correctness battery over concrete and symbolic ranges all
returns the expected results, e.g.:
- `(str.in_re "b" (re.range "a" "c"))` → `sat`, `(str.in_re "d"
(re.range "a" "c"))` → `unsat`
- `(str.in_re x (re.range x x))` → `sat`; with `(= (str.len x) 2)` →
`unsat`
- `(str.in_re "b" (re.range x y))` → `sat`; with `(str.< y x)` → `unsat`
- `(str.in_re "" (re.range x y))` → `unsat`; `(str.in_re "ab" (re.range
"a" "c"))` → `unsat`
The pre-existing concrete-range derivative fast path is unchanged.
### Note on the model value (benign, unrelated to this fix)
The model value differs from the recorded oracle: current z3 prints
`((tmp_str0 "A"))` whereas the oracle recorded `((tmp_str0 "\u{0}"))`.
Both are valid single-character models (the formula has many). This
difference is **pre-existing and unrelated to this fix**: even a bare
`(assert (= (str.len x) 1))` yields `"A"` on current z3. It stems from
the seq/char theory's default character assignment for
otherwise-unconstrained characters (`theory_char.cpp` assigns fresh
characters starting from `'A'`), not from range handling. I deliberately
did **not** force the character to `\u{0}` — adding `x = "\u{0}"` would
be unsound over-constraining, and changing the global default character
is out of scope for this soundness fix and would perturb unrelated
models. The output is therefore semantically equivalent to the oracle
(same `sat` verdict and reason-unknown) but not byte-identical.
---
*Draft for human review. Diagnosed and fixed by the
`snapshot-regression-fixer` maintenance workflow.*
> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/28502614658)
· 890.7 AIC · ⌖ 46.8 AIC · ⊞ 9K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+snapshot-regression-fixer%22&type=pullrequests)
<!-- gh-aw-agentic-workflow: Fix a Z3 snapshot-regression divergence,
engine: copilot, version: 1.0.63, model: claude-opus-4.8, id:
28502614658, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/28502614658 -->
<!-- gh-aw-workflow-id: snapshot-regression-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/snapshot-regression-fixer
-->
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
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>
`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>
