Port seq_monadic to the split_set branch, reimplemented against the
cont_regex / split / split_manager API. Element-sort agnostic: relies on
the derivative engine and th_rewriter, no character-specific reasoning.
- Global derivative-transition graph reused across regexes (intern_state /
expand_state / build_graph) so states, nullability and cofactor successors
are computed once.
- embed(r) = <concat(r, epsilon), epsilon>; the epsilon accept-state marks the
membership (nullable) case uniformly.
- intersect handles general cont_regex, including non-epsilon reach targets N
(membership BFS + product-reachability paths).
- No budget / reset_pin.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 34aa9af0-4977-411d-aaa7-7cb81cc4e9f8
When a term column x - y is fixed to 0 (e.g. from t <= ca and t >= ca),
theory_lra previously discovered the implied equality x = y only lazily via
assume_eqs() during final_check. On the FP fuel-recursive axiom in issue #10065
this discovery is starved by E-matching, which unfolds the recursion and
bit-blasts an exploding FP subproblem before the branch closes.
Add propagate_offset_eq() to detect a fixed 2-variable offset term with opposite
unit-scaled coefficients and propagate the operand equality x = y directly to the
core, so congruence closure merges dependent terms immediately. This mirrors the
offset-row propagation performed by theory_arith (propagate_cheap_eq) and matches
its behavior on this benchmark (timeout -> unsat 0.06s, 2 quant-instantiations).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 726c4e71-03ff-45f6-8322-5253254e1d7e
## 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>
