## Problem
A QF_NIA benchmark (`From_T2__ex16.t2__p22243_terminationG_0.smt2`, run
with `-T:200 model_validate=true`) crashes with SIGSEGV inside nlsat.
## Root cause
In `algebraic_numbers::manager:👿:compare_core`, the
interval-separation workaround computed the isolating intervals of `a`
and `b` with:
```cpp
if (get_interval(a, la, ua, precision) &&
get_interval(b, lb, ub, precision)) { ... }
```
`&&` short-circuits: when `a` is **rational**, `get_interval(a, ...)`
finds the exact root and returns `false`, so `get_interval(b, ...)`
never runs and `b`'s bounds `lb`/`ub` stay **0**. Those bounds are used
*unconditionally* below the `if` (in the `compare(cell_a, u_b)` /
`compare(cell_b, l_a)` checks), so `a` was effectively compared against
`0`, producing an incorrect and self-inconsistent sign (`compare`
returned `+1` while `<`, `=`, `>` were all false).
Concretely, comparing `c = 39017/131072` (rational) with `d ≈
0.297676176` (root of a quadratic) returned `c > d`, though `c < d`.
Downstream, this made nlsat's `interval_set::is_full` miss full coverage
of ℝ, so `pick_in_complement` was invoked on an empty complement and
read `s->m_intervals[UINT_MAX]` — a crash guarded only by a
release-stripped `SASSERT` (`nlsat_interval_set.cpp`).
## Fix
Compute both intervals unconditionally so `b`'s bounds are always valid
before they are used.
## Validation
- The crashing benchmark now returns `unsat` (verified on both macOS and
a Linux `RelWithDebInfo` build where the SIGSEGV was originally
reproduced under gdb).
- Unit tests pass: `algebraic`, `upolynomial`, `polynomial`, `nlsat`.
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
reduce_core looped with while (true) and read p = todo.back() with no
empty check, exiting only when it reached a hypothesis-free sub-proof of
false. When hypothesis reduction cannot close all hypotheses on the root
proof, todo drains and todo.back() reads past the end of the vector,
producing a heap-use-after-free (SIGSEGV in Fixedpoint.query with
spacer.keep_proxy=false). Whether the root closes depends on search order,
making the crash nondeterministic / seed-dependent.
Bound the loop by todo emptiness, track the reduced root across cache-hit
pops, and return it if the loop drains without hitting the false-subproof
early return.
Verified on the issue #10123 benchmark: the UAF is eliminated across
spacer.random_seed 0/3/7/13/42/99, all returning unsat.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 726c4e71-03ff-45f6-8322-5253254e1d7e
## Summary
Optimizes `lp::static_matrix<..>::remove_element`, reported as a hotspot
in
[Z3Prover/bench#3143](https://github.com/Z3Prover/bench/discussions/3143)
(the #1 exclusive-time function, ~19.6%, on
`inputs/issues/iss-5131/bug-1.smt2`).
`remove_element` uses swap-remove but **deep-copied** the relocated tail
coefficient:
```cpp
auto & rc = row_vals[row_offset] = row_vals.back(); // copy from the tail
```
In namespace `lp`, `mpq` is a typedef for the copyable `rational`, so
this copy-assign allocates a fresh bignum whenever the **source (the
tail)** is big — matching the `malloc`/`_int_malloc` entries in the
reported profile. The tail element is `pop_back`'d immediately
afterwards, so the allocation is wasteful.
## Change
A copy-assign allocates only when the **source** is big
(`mpz_manager::set` → `big_set`). So relocate the tail coefficient by
**swapping** exactly in that case — stealing its already-allocated
storage, zero `malloc`. When the tail is small, a plain copy never
allocates and is cheaper than swapping the `mpz` internals; the
destination's size is irrelevant. The column-cell relocation is
unchanged (a `column_cell` carries no coefficient).
Single-file change; no new parameters.
## Benchmarks
A/B produced by toggling the new code path against the original
deep-copy (via a temporary parameter, not included here).
- **rise-runner-2** (initial `is_big()||is_big()` variant): QF_LIA_small
neutral; certora identical outcomes, −1.5% paired solve-time.
- **128-core Linux box**, `run_on_dir.py`, `-max_workers 32` (final
tail-only variant):
| Set | Files | `-T` | Solved (new = orig) | Avg-time ratio new/orig |
Correctness |
|---|---|---|---|---|---|
| QF_LIA (SMT-LIB) | 6947 | 20s | 5817 ≈ 5815 | 1.00000 | identical (±2
timeout-edge) |
| certora | 308 | 120s | 186 = 186 | 0.9977 | identical, 0 unique
timeouts |
| QF_LRA (SMT-LIB 2025) | 1753 | 120s | 1552 = 1552 | 0.9985–0.9991 |
identical, 0 real regressions |
Consistently **correctness-neutral and marginally faster** (~0.1–0.5%)
on large-coefficient LP sets, flat on small-coefficient inputs. The
per-`remove_element` allocation saved is small relative to total solve
time, so the whole-solver delta is a fraction of a percent — a clean
micro-optimization with no downside.
## Validation
- `make`/`ninja` build clean; `test-z3 /a` — 92/92 pass.
- Baseline vs patched output byte-identical on the reported benchmark;
identical solve sets across all three benchmark suites above.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Implement check_mod_congruence in nla_divisions: for two mod-atoms
sharing a (possibly symbolic) divisor y, emit the model-guided tautology
div(x,y) - div(s,y) = delta => mod(x,y) - mod(s,y) = (x - s) - delta*y.
This discharges linear congruences over a symbolic modulus that the
nonlinear core did not otherwise isolate. Thread the div(x,y) variable
through add_divisibility (nla_core/nla_solver/nla_divisions) and
register it in theory_lra for symbolic-divisor mod terms.
Solves FStar.BitVector-1 (0.7s) and FStar.Matrix-1 (1.6s), previously
300s timeouts; all 92 unit tests pass.
Copilot-Session: 726c4e71-03ff-45f6-8322-5253254e1d7e
---------
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
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>
Sound by array extensionality when a is independent of the bound
variables. Implemented as array_rewriter::mk_lambda_core and wired into
th_rewriter::reduce_quantifier alongside the ground-lambda case.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
rules_foreign_cc expects libraries under its default lib output
directory. GNUInstallDirs may instead select lib64, causing Bazel to
reject an otherwise successful CMake build because its declared output
is missing.
Share the default CMake arguments between the static and dynamic targets
and set CMAKE_INSTALL_LIBDIR to lib.
The nightly workflow’s `Publish to test.PyPI` job fails because
test.PyPI rejects uploaded macOS wheels tagged `macosx_13_3_*`. This
change keeps the validation publish path working by rewriting
unsupported macOS wheel tags to a supported form during that specific
upload step.
- **Root cause reflected in workflow behavior**
- `publish-test-pypi` currently uploads all artifacts from
`PythonPackages`, including macOS wheels that test.PyPI does not accept.
- **Workflow change (surgical)**
- In `.github/workflows/nightly.yml`, added a pre-upload rewrite step in
`publish-test-pypi` to rename wheel tags from `macosx_13_3_*` to
`macosx_13_*` in `dist/`.
- Left artifact production unchanged; only the filenames used for the
test.PyPI upload are adjusted.
- **Effect on release flow**
- test.PyPI upload continues for sdist + Linux/Windows wheels and now
includes rewritten macOS wheels.
- Nightly macOS artifacts remain built and available through existing
artifact/release paths.
```yaml
- name: Rewrite macOS wheel tags unsupported by test.PyPI
run: |
for whl in dist/*-macosx_13_3_*.whl; do
[ -e "$whl" ] || continue
mv "$whl" "${whl/macosx_13_3_/macosx_13_}"
done
ls -l dist
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The `Release Build` workflow still targeted macOS 13.0 for the x64/arm64
packaging jobs, while the codebase now relies on libc++ functionality
that is only available with a 13.3 deployment target. This updates the
release workflow to use the same macOS target configuration already
applied in `nightly.yml`.
- **Release workflow**
- Raise `MACOSX_DEPLOYMENT_TARGET` from `13.0` to `13.3` for both
`mac-build-x64` and `mac-build-arm64`
- Update the packaging target passed to `mk_unix_dist.py` from
`--os=osx-13.0` to `--os=osx-13.3`
- **Config alignment**
- Bring `release.yml` in sync with the existing nightly macOS fix so
both workflows build against the same minimum macOS version
```yaml
env:
MACOSX_DEPLOYMENT_TARGET: "13.3"
run: python scripts/mk_unix_dist.py --arch=x64 --os=osx-13.3
```
---------
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 `release-notes-updater` agent job was failing with HTTP 401 on every
Copilot API inference request because the GitHub Actions token lacked
`copilot-requests: write`.
## Changes
- **`release-notes-updater.md`**: Replace `permissions: read-all`
shorthand with an explicit permissions object that includes
`copilot-requests: write`
- **`release-notes-updater.lock.yml`**: Recompiled via `gh aw compile`
```yaml
# Before
permissions: read-all
# After
permissions:
contents: read
issues: read
pull-requests: read
discussions: read
copilot-requests: write
```
`read-all` expands all scopes to read but does not grant
`copilot-requests: write`, which is the permission required for the
GitHub Actions token to authenticate with the Copilot API proxy.
---------
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>
`ASSERTION VIOLATION` at `bv2int_translator.h:72` when using
`smt.bv.solver=2` with formulas containing `abs` (or other arith
expressions that rewrite to ITE with arith predicates).
**Root cause**
`ensure_translated` skips adding sub-expressions of boolean non-BV nodes
to the `todo` list — correct, since the base theory owns them in plugin
mode. However, `translate_expr`'s early-return only covered
`basic_family_id` booleans, not non-basic ones (e.g.,
`arith_family_id`).
When `(abs f)` is rewritten by the arith rewriter to `(ite (>= f 0) f (-
f))`, the predicate `(>= f 0)` ends up in `todo` (as a child of the
ITE), but its own children (e.g., the integer literal `0`) are not
added. `translate_expr` then calls `translated(0)` on an unmapped
expression, firing `SASSERT(r)`.
Reproducer:
```smt2
(declare-const f Int)
(assert (= 0 (mod 0 (bv2nat ((_ int_to_bv 1) (abs f))))))
(check-sat)
; z3 test.smt2 smt.bv.solver=2 → ASSERTION VIOLATION (before fix)
```
**Fix**
Extend the early-return in `translate_expr` to match
`ensure_translated`'s skip condition — all boolean non-BV expressions in
plugin mode map to themselves:
```cpp
// before
if (m_is_plugin && ap->get_family_id() == basic_family_id && m.is_bool(ap)) {
// after
if (m_is_plugin && m.is_bool(ap) && ap->get_family_id() != bv.get_family_id()) {
```
BV boolean predicates (`bvule`, etc.) are unaffected — they still route
through `translate_bv`.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
`Expr.getSort()` on a constant with an `EnumSort` sort returns a
`DatatypeSort`, causing `ClassCastException` when enum-specific methods
are called.
```java
Context ctx = new Context();
EnumSort<Foo> enumSort = ctx.mkEnumSort("my-enum", "e1", "e2");
Expr<EnumSort<Foo>> c = ctx.mkConst("my-const", enumSort);
c.getSort().getName(); // ClassCastException — getSort() returns DatatypeSort, not EnumSort
```
### Changes
- **`Sort.java`**: In `Sort.create()`, detect enum sorts at the
`Z3_DATATYPE_SORT` case by checking whether all constructors have arity
0 — matching Z3's own `util::is_enum_sort` logic in
`datatype_decl_plugin.cpp`. Return `EnumSort<>` when true,
`DatatypeSort<>` otherwise.
- **`EnumSort.java`**: Add package-private `EnumSort(Context ctx, long
obj)` constructor so an `EnumSort` can be instantiated from an existing
native sort handle (analogous to `DatatypeSort(Context ctx, long obj)`).
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Fixes the divergence in issue #7464: formulas involving `mod`/`div` by a
**variable** divisor could send `smt.arith.solver=6` into a
non-terminating nonlinear search.
Minimal reproducer (UNSAT, previously timed out; now solved in <0.5s):
```smt2
(declare-fun V () Int)
(declare-fun n () Int)
(declare-fun l () Int)
(assert (and (> V 0) (= 0 (mod n 2)) (= (div n 2) (div n l)) (= 0 (mod (div n l) V))))
(assert (distinct 0 (mod n V)))
(check-sat)
```
## Root cause
A variable-divisor `mod n V` is axiomatized by the Euclidean identity
`n = V*(n div V) + (n mod V)`. The `V*(n div V)` term is nonlinear, so
arith.solver=6
hands the problem to the nlsat/Gröbner branch, which branches on values
of `V` with no
termination bound and diverges.
## Fix
Add a **linear divisibility closure** lemma in `nla_divisions`:
> `mod(a, y) = 0 & x = c*a` (c an integer constant) ⟹ `mod(x, y) = 0`.
The emitted clause
```
(x - c*a != 0) \/ (mod(a, y) != 0) \/ (mod(x, y) = 0)
```
is a **tautology for every integer `c`**, so mining a candidate `c =
val(x)/val(a)` from
the current model can never be unsound. It is only emitted when all
three literals are
false in the current model, so the clause is a genuine
conflict/propagation and always
makes progress. This lets the theory refute the instance directly
instead of entering the
divergent nonlinear branch.
Variable-divisor `mod` terms were previously **not registered** in nla
at all; they are now
registered into a new `m_divisibility` list in `theory_lra`, so the
reasoner can pair a
violated `mod(x, y)` with a satisfied `mod(a, y)` of the same divisor.
## Changes
- `src/math/lp/nla_divisions.{h,cpp}` — new `m_divisibility` list
`{r=mod, x=dividend, y=divisor}`, `add_divisibility(...)`, and
`check_linear_divisibility()`; invoked from `divisions::check()`.
- `src/math/lp/nla_core.h`, `src/math/lp/nla_solver.{h,cpp}` —
forwarding of `add_divisibility`.
- `src/smt/theory_lra.cpp` — register variable-divisor `mod` into the
divisibility list.
## Validation
- `min.smt2` → `unsat` in 0.46s, minimized core → 0.15s (were timeouts).
- Soundness: 350 differential fuzz formulas (arith.solver=6 vs
arith.solver=2), **0 mismatches**.
- Spot checks correct (divisor-3 variant → unsat; non-divisible variants
→ sat).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
`decl_collector::visit_sort` did not collect sorts with `poly_family_id`
(type variables created via `mk_type_var` / `declare-type-var`), so
`solver::display` and `ast_pp_util::display_decls` never emitted type
variable declarations before referencing them — producing invalid
SMT-LIB2 output.
## Changes
- **`src/ast/decl_collector.h`**: added a dedicated `lim_svector<sort*>
m_type_vars` field (separate from `m_sorts`) with a `get_type_vars()`
getter; `reset()` clears it; `push()`/`pop()` maintain its scope.
- **`src/ast/decl_collector.cpp` — `visit_sort`**: sorts with
`poly_family_id` are now pushed to `m_type_vars` instead of `m_sorts`,
keeping type variables distinct from uninterpreted sorts:
```cpp
if (m.is_uninterp(n))
m_sorts.push_back(n);
else if (fid == poly_family_id)
m_type_vars.push_back(n);
```
- **`src/ast/ast_pp_util.h`**: added a `stacked_value<unsigned>
m_type_vars` cursor to track which type variables have already been
printed.
- **`src/ast/ast_pp_util.cpp` — `display_decls`**: emits
`(declare-type-var <name>)` for each collected type variable before
other sort declarations; `reset()`/`push()`/`pop()` maintain the new
cursor.
**Example** — given `(declare-type-var A)(declare-fun f (A) A)`, the
dump now correctly produces:
```smt2
(declare-type-var A)
(declare-fun f (A) A)
(assert ...)
```
The output round-trips cleanly through the Z3 parser.
---------
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>
`z3_add_install_tactic_rule` unconditionally called `file(WRITE)` during
CMake configure, updating `install_tactic.deps`'s mtime on every
reconfiguration — even when the content was identical. Since
`install_tactic.cpp` lists `install_tactic.deps` as a dependency, any
CMake reconfigure (e.g. touching `src/api/ml/CMakeLists.txt`) caused a
full rebuild of the tactic installation target.
## Change
- **`cmake/z3_add_component.cmake` — `z3_add_install_tactic_rule`**:
Replace unconditional `file(WRITE)` with a read-and-compare guard; the
deps file is only rewritten when its content actually changes.
```cmake
# Before
file(WRITE "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.deps" ${_tactic_header_files})
# After
set(_install_tactic_deps_file "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.deps")
if (EXISTS "${_install_tactic_deps_file}")
file(READ "${_install_tactic_deps_file}" _install_tactic_deps_old)
else()
set(_install_tactic_deps_old "")
endif()
if (NOT _install_tactic_deps_old STREQUAL "${_tactic_header_files}")
file(WRITE "${_install_tactic_deps_file}" "${_tactic_header_files}")
endif()
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The TPTP frontend was not forcing `pi.avoid_skolems=false`, so TPTP
problems could be solved with the default pattern-inference behavior
instead of the intended frontend-specific setting. This change applies
the override directly to the solver used by TPTP runs.
- **What changed**
- After constructing the TPTP solver, the frontend now sets
`pi.avoid_skolems=false` via solver parameters before `check_sat`.
- The override is scoped to the TPTP solver instance instead of mutating
process-global parameter state.
- **Why this shape**
- Keeps the TPTP behavior explicit at the point where the solver is
created.
- Avoids leaking the parameter change into unrelated solver contexts.
- **Code sketch**
```c++
ctx.set_solver_factory(mk_smt_strategic_solver_factory());
params_ref solver_params;
solver_params.set_bool("pi.avoid_skolems", false);
ctx.get_solver()->updt_params(solver_params);
```
---------
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>
Multiple agentic workflows were failing at runtime with
`MODULE_NOT_FOUND` for `merge_awf_model_multipliers.cjs` under
`${RUNNER_TEMP}/gh-aw/actions`. The lock workflows had stale generated
runtime steps that no longer matched the current `gh-aw` actions bundle.
- **Root cause**
- Generated `.lock.yml` workflows referenced a removed script:
- `node "${RUNNER_TEMP}/gh-aw/actions/merge_awf_model_multipliers.cjs"`
- **Change**
- Recompiled all agentic workflow sources (`.github/workflows/*.md`)
with current `gh aw` tooling.
- Checked in regenerated lock artifacts:
- `.github/workflows/*.lock.yml`
- `.github/aw/actions-lock.json`
- Result: stale `merge_awf_model_multipliers.cjs` invocations were
eliminated from generated workflows.
- **Representative diff shape**
```yaml
# removed from generated lock workflows
- GH_AW_MODEL_MULTIPLIERS_PATH="/tmp/gh-aw/model_multipliers.json" \
node "${RUNNER_TEMP}/gh-aw/actions/merge_awf_model_multipliers.cjs"
```
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This PR adds a first-class Python API helper for expressing regex
constraints in familiar Python regex syntax and translating them into Z3
regex terms. The translator is implemented as a separate module
(`z3regex.py`) as requested, keeping regex conversion logic isolated
from core API files.
- **New Python regex translator module**
- Adds `src/api/python/z3/z3regex.py`.
- Introduces `regex_to_re(pattern, flags=0, ctx=None)` to convert parsed
Python regex constructs into Z3 regex expressions.
- Supports core regular constructs (literals, classes/ranges,
alternation, grouping, quantifiers, categories, wildcard).
- Raises `NotImplementedError` for unsupported non-regular constructs
(e.g., features outside regular languages).
- **API/package integration**
- Exposes the module via `src/api/python/z3/__init__.py`.
- Includes `z3/z3regex.py` in Python binding file copy/install flow in
`src/api/python/CMakeLists.txt`.
- **Doctest entrypoint support**
- Extends `src/api/python/z3test.py` with `z3regex` mode so translator
doctests can be run consistently with existing Python API doctest flows.
```python
from z3 import *
from z3.z3regex import regex_to_re
x = String("x")
r = regex_to_re(r"(ab|cd)+\d{2}")
s = Solver()
s.add(InRe(x, r))
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
The Nightly release occasionally exposed a mismatch between the commit
shown on the release page and the downloaded “Source code” archive. Root
cause was non-deterministic `Nightly` tag/release state during publish.
- **Deterministic Nightly tag lifecycle**
- Serialize Nightly workflow runs with a dedicated concurrency group to
prevent overlapping tag/release mutations.
- Replace best-effort cleanup with explicit release-exists checks and
failure-on-cleanup-error behavior.
- Remove orphan `Nightly` tags even when no release exists.
- **Pin release to the exact workflow commit**
- Force-update `Nightly` to `${{ github.sha }}` and push it before
release creation.
- Verify remote tag SHA (including annotated-tag dereference shape)
matches `${{ github.sha }}`.
- Create release with `--verify-tag` so source archives are generated
from the validated tag, not an implicit/stale target.
- **Workflow behavior change (deploy section)**
```yaml
concurrency:
group: nightly-release
cancel-in-progress: false
```
```bash
git tag -f Nightly "${{ github.sha }}"
git push --force origin refs/tags/Nightly
gh release create Nightly --verify-tag ...
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Creating and disposing `Context` instances causes unbounded native
memory growth (~12 GB for 100k contexts) because `NativeContext` had no
finalizer — if `Dispose()` was never called, the native Z3 context
leaked permanently. Additionally, both `Context` and `NativeContext` had
delegate lifetime and thread-safety issues in their disposal paths.
## `NativeContext.cs`
- **Add missing finalizer** `~NativeContext() { Dispose(); }` — the root
cause of permanent leaks when callers don't explicitly dispose
- **Atomic disposal** via `Interlocked.Exchange(ref m_ctx, IntPtr.Zero)`
— prevents double-free when `Dispose()` is called concurrently (e.g.
user code + finalizer race)
- **Delegate lifetime** — capture `errHandler` locally +
`GC.KeepAlive(errHandler)` after `Z3_del_context`; the GC could
otherwise collect the error handler callback before the native
destructor finishes
- **Remove dead code** — `GC.SuppressFinalize` in `InitContext()` and
`GC.ReRegisterForFinalize` in `Dispose()` were both no-ops (no finalizer
existed); the latter would have caused infinite finalization with the
new finalizer
- **GC memory pressure** — `GC.AddMemoryPressure(8MB)` on init /
`GC.RemoveMemoryPressure(8MB)` on dispose, guarded by
`m_memPressureAdded` flag, so the GC schedules finalizers promptly when
contexts accumulate
## `Context.cs`
- **Thread-safe disposal** — capture `ctx` and `errHandler` inside the
existing `lock(this)` block; previously both were read outside the lock,
allowing two concurrent callers to both capture the same non-zero `ctx`
and double-free it
- **Delegate lifetime** — same `errHandler` + `GC.KeepAlive` pattern as
`NativeContext`
- **`GC.SuppressFinalize` placement** — moved inside the `if (m_ctx !=
IntPtr.Zero)` block, before cleanup, per .NET best practice
- **GC memory pressure** — same add/remove pattern, conditioned on
`!is_external` via `m_memPressureAdded` flag
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
