The "Ubuntu with OCaml on z3-static" CI job intermittently fails with
`Fatal error: exception End_of_file` from the OCaml bytecode linker when
compiling `ml_example_static.byte`.
## Root cause
`ocamlfind install z3-static build/api/ml/* build/libz3-static.a`
auto-recognizes `dllz3ml-static.so` (starts with `dll`) as a C stub and
copies it to `stublibs`, but without an explicit `-dll` flag it **does
not update `ld.conf`**—confirmed by the CI warning:
```
ocamlfind: [WARNING] You have installed DLLs but the directory .../stublibs is not mentioned in ld.conf
```
`ocamlc` searches `ld.conf` for stub DLLs at bytecode link time; the
missing entry causes `End_of_file`. The non-static job is unaffected
because it passes `-dll build/libz3.*` explicitly, which triggers the
`ld.conf` update as a side-effect.
## Fix
After `ocamlfind install`, append the `stublibs` path to `ld.conf` if
absent:
```bash
STUBLIBS="$(dirname "$(ocamlfind printconf destdir)")/stublibs"
LDCONF="$(ocamlfind printconf ldconf)"
if [ -d "$STUBLIBS" ] && ! grep -qF "$STUBLIBS" "$LDCONF" 2>/dev/null; then
echo "$STUBLIBS" >> "$LDCONF"
fi
```
Idempotent; uses `ocamlfind printconf` to avoid hardcoded paths.
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>
## Summary
Follow-up to #10001 addressing @NikolajBjorner's review comment:
> isn't this nearly identical AI generated code to the other file? There
has to be some modular approach to deal with sorting vectors?
#10001 introduced two nearly-identical copies of a bounds-safe,
mutation-aware index-permutation merge sort:
- `algebraic_numbers.cpp::merge_sort_roots_perm`
- `nlsat/levelwise.cpp::merge_sort_perm`
Both exist because the comparator (`anum_manager::compare`/`lt`) is
**not pure**: it mutates the algebraic numbers it compares (refining
isolating intervals) and may throw on the resource limit, which makes
`std::sort` undefined behavior (the original SIGSEGV).
## Change
Extract the algorithm into a single shared helper
`util/index_sort_with_mutations.h` (`stable_index_merge_sort`). The long
rationale for why `std::sort` is unsafe and merge sort is safe now lives
in exactly one place. Both call sites become thin wrappers that build
the scratch buffer and forward their local comparator.
No behavioral change: same stable O(n log n) merge sort over an index
permutation.
## Verification
CMake/Ninja Release build:
- `test-z3 /seq algebraic_numbers` — PASS
- `test-z3 /seq algebraic` — PASS
- NRA/NIA smoke solves with `nlsat.lws=true` return expected sat/unsat.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Replace goto-based control flow in get_cube_delta_for_term with an
all_ok flag for structured early-exit. Use aggregate initialization for
flip_candidate, constructor-based vector sizing for occs, brace
initialization for pairs in add_edge_rows_for_term.
No functional changes - all lcube tests pass.
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
## Summary
Alternative to #9991. Instead of disabling `nlsat.lws` by default, this
**fixes the underlying bug** so levelwise single-cell projection stays
enabled.
## Root cause
The crash was reproduced on the QF_NIA benchmark from #9991
(`20170427-VeryMax/ITS/From_AProVE_2014__Round3.jar-obl-8__p11898_terminationG_0.smt2`,
~40% SIGSEGV at `-T:20`). A core-dump backtrace points at:
```
mpbq_manager::le (mpbq.cpp:362)
algebraic_numbers::manager:👿:compare (algebraic_numbers.cpp:1913) c = 0xea24052d29f2d500 <- wild pointer
algebraic_numbers::manager:👿:compare (algebraic_numbers.cpp:2128)
nlsat::levelwise::impl::root_function_lt (levelwise.cpp:949)
... std::__unguarded_linear_insert ... <- OOB read
std::sort
nlsat::levelwise::impl::sort_root_function_partitions
```
The comparator (`root_function_lt` → `anum_manager::compare`, and
`anum_manager::lt`) **refines the isolating intervals of the algebraic
numbers it compares** and may **hit the resource limit (throwing)**
mid-comparison. Both make the order it induces non-deterministic / not a
strict weak ordering across a single `std::sort` — undefined behavior.
libstdc++'s *unguarded* insertion pass then walks past `begin()` and
dereferences a wild anum cell → SIGSEGV. This only fires when a timeout
interrupts levelwise, explaining the non-determinism (`signal-11`).
## Fix
Replace the two affected `std::sort` calls
(`sort_root_function_partitions` and `add_adjacent_root_resultants`)
with a **bounds-checked insertion sort over an index permutation**. A
fully guarded insertion sort can never read out of bounds regardless of
comparator consistency, and unwinds cleanly if `compare` throws on
cancellation. The partitions sorted here are small, so the O(n²) cost is
negligible.
`nlsat.lws` stays `true`.
## Verification
On the Linux repro box (Ubuntu 24.04, g++ 13), RelWithDebInfo:
- **Before:** ~40% SIGSEGV (e.g. 5/16 runs at `-T:20`).
- **After:** **0/30** SIGSEGV; results are `unsat`/`timeout`.
- Sanity batch over 25 QF_NIA/VeryMax/ITS files: no crashes, expected
sat/unsat/timeout mix.
- `model_validate=true` full solve still returns `unsat`.
---------
Co-authored-by: Copilot <223556219+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>
The Go bindings rely on finalizers to release Z3 references, which can
run during concurrent GC and trigger unsafe decref behavior in shared
contexts. This change aligns Go with other managed bindings by enabling
concurrent decref support at context creation time.
- **Context initialization**
- Call `Z3_enable_concurrent_dec_ref` in both Go context constructors:
- `NewContext()`
- `NewContextWithConfig(cfg *Config)`
- This ensures AST/object finalizer decrefs are handled under Z3’s
concurrent dec-ref mode.
- **Go binding docs**
- Updated Go README memory-management section to explicitly document
that contexts enable concurrent dec-ref for finalizer-driven decref
paths.
- **Focused regression coverage**
- Added a small Go test (`z3_context_test.go`) that exercises
`NewContext` through a basic SAT flow, ensuring context construction and
normal solver usage remain consistent.
```go
func NewContext() *Context {
ctx := &Context{ptr: C.Z3_mk_context_rc(C.Z3_mk_config())}
C.Z3_enable_concurrent_dec_ref(ctx.ptr)
runtime.SetFinalizer(ctx, func(c *Context) {
C.Z3_del_context(c.ptr)
})
return ctx
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.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>
## Summary
Fixes a hang (wall-clock timeout) in the native parallel SMT solver when
a cube is incomplete for a reason that cannot change. Originating
discussion: https://github.com/Z3Prover/bench/discussions/2746
Benchmark: `iss-3707/bug-1.smt2` (`QF_NRA`, runs with
`parallel.enable=true`).
## Divergence
The recorded oracle vs. current z3 (`z3 -T:20`):
```diff
-(incomplete (theory difference-logic))
-unknown
+timeout
```
z3 should terminate with `unknown` (incomplete theory) but instead spins
until the 20s timeout.
## Root cause
In `src/smt/smt_parallel.cpp` the per-cube worker handled an `l_undef`
cube by unconditionally calling `update_max_thread_conflicts()` and
re-splitting/re-checking. That only helps when the cube was abandoned at
the per-cube conflict limit (`max-conflicts-reached`). When the cube is
incomplete for a permanent reason (incomplete theory, quantifiers,
resource limits), the verdict never changes, so the worker re-checks the
same cube forever. The `batch_manager` had no `unknown` terminal state,
so `get_result()` could only end as sat/unsat/exception — there was no
way to settle on `unknown`, hence the hang. This is the `smt_parallel`
analogue of the `parallel_tactical.cpp` regression fixed earlier.
## Fix
Minimal, mirroring the tactic-side fix:
- add an `is_unknown` batch-manager state + `m_reason_unknown`;
- a worker reporting `l_undef` whose `last_failure` is not
`max-conflicts-reached` calls `set_unknown(reason)` and stops
re-splitting;
- `set_sat`/`set_unsat` may still override `is_unknown` so a definitive
answer wins;
- `get_result()` maps `is_unknown -> l_undef` and the reason propagates
to the parent context.
## Validation
Rebuilt z3 (`make -C build -j16`) and re-ran the benchmark 5× with
`-T:20`. Every run finished in well under the timeout with output
matching the oracle byte-for-byte:
```
(incomplete (theory difference-logic))
unknown
```
Created as a **draft** for human review.
> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/28358375255)
· 553.9 AIC · ⌖ 27.2 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:
28358375255, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/28358375255 -->
<!-- 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>
`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
Fixes a `psmt` (parallel SMT tactic) regression where the solver hangs
to a wall-clock timeout instead of returning `unknown` on formulas whose
root cube is genuinely undetermined by an incomplete theory.
- **Originating discussion:**
https://github.com/Z3Prover/bench/discussions/2735
- **Benchmark:** `iss-3044/bug-1.smt2` (from [Z3 issue
#3044](https://github.com/Z3Prover/z3/issues/3044))
```smt2
(declare-fun a (Int) Bool)
(declare-fun b (Int) Bool)
(assert (distinct a b))
(check-sat-using psmt)
```
## Divergence
The recorded oracle (expected) vs. current z3 (combined stdout+stderr,
`-T:20`):
```diff
-(incomplete (theory array))
-unknown
+timeout
```
## Root cause
The rewritten parallel tactic (`src/solver/parallel_tactical.cpp`,
introduced in #9824/#9825) hangs on this input.
In the worker `run()` loop, every `l_undef` cube result was treated as
if the per-cube **conflict limit** had been reached: the worker
escalated the per-thread conflict budget (`update_max_thread_conflicts`)
and re-checked / re-split the same cube. When the `l_undef` actually
comes from **theory incompleteness** (here, the array theory cannot
decide `(distinct a b)` over `Int -> Bool`) rather than the conflict
limit, the verdict never changes, so the worker re-checks the same cube
forever.
Compounding this, the `batch_manager` state machine had **no terminal
`unknown` state** — the only way to finish was for some worker to prove
`sat`/`unsat`, which is impossible for a root-level theory-incomplete
formula. The combination produced an infinite loop and a wall-clock
timeout.
The pre-rewrite parallel tactic avoided this: its `giveup()` detected
reasons starting with `(incomplete` / `(sat.giveup`, reported a soft
undef, and echoed the reason to `verbose_stream()`.
## Fix
All changes are confined to `src/solver/parallel_tactical.cpp` (47
insertions, 4 deletions):
1. **Distinguish genuine incompleteness from conflict-limit
exhaustion.** In the worker `l_undef` case, only `reason_unknown() ==
"max-conflicts-reached"` benefits from escalating the budget /
splitting. For any other reason (incomplete theory, quantifiers,
lambdas, resource limits, ...) re-checking is futile, so the worker
records a sound `unknown` and stops working the branch.
2. **Add a terminal `is_unknown` batch-manager state** (`set_unknown`,
`get_result() -> l_undef`, reason storage). It is a *soft* result: it
does not cancel the other workers, and a definitive `sat`/`unsat`
verdict from another branch may still override it (the
`set_sat`/`set_unsat` guards now permit overriding `is_unknown`). All
`set_unsat` call sites are global formula-unsat (core ⊆ assumptions, or
independent of the tested backbone literal), so the override is sound;
tree-closure unsat remains guarded by `is_running` and cannot fire
because the undef leaf stays open.
3. **Restore the reason output.** The captured `reason_unknown` is
propagated to the result goal and echoed to `verbose_stream()`,
reproducing the `(incomplete (theory array))` line that the sequential
path / old parallel tactic emitted.
## Validation
Rebuilt the `./z3` checkout (`./configure && make -C build -j16`) and
re-ran the benchmark with the freshly built binary using the same
options the snapshot capture uses (`-T:20`, combined stdout+stderr):
```
$ z3 inputs/issues/iss-3044/bug-1.smt2 -T:20
(incomplete (theory array))
unknown
```
This matches the recorded `bug-1.expected.out` oracle **byte-for-byte**,
and the benchmark now completes in ~0.5s (was: timeout). Verified stable
across 8 consecutive runs. Basic `psmt` `sat`/`unsat` checks continue to
produce correct results.
Opened as a **draft** for human review.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/28313246856)
· 5.7K AIC · ⌖ 85.8 AIC · ⊞ 41.2K ·
[◷](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.60, model: claude-opus-4.8, id:
28313246856, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/28313246856 -->
<!-- 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>
## Problem
The [master WebAssembly
Build](https://github.com/Z3Prover/z3/actions/runs/28306680131) fails
with:
```
../src/solver/parallel_tactical.cpp:59:9: error: redefinition of 'mk_parallel_tactic'
59 | tactic* mk_parallel_tactic(solver* s, params_ref const& /* p */) {
../src/solver/parallel_tactical.cpp:55:9: note: previous definition is here
```
## Cause
Commit 7564ccc3f (an unrelated lar_solver change) accidentally renamed
the dead `mk_parallel_tactic2` stub to `mk_parallel_tactic`, leaving two
identical definitions inside the `#ifdef SINGLE_THREAD` block. The WASM
build defines `SINGLE_THREAD`, so it hits the redefinition.
## Fix
`mk_parallel_tactic2` and its `non_parallel_tactic2` class were never
referenced anywhere. This removes the dead stub and orphaned class,
keeping the single `mk_parallel_tactic` that degrades to
`mk_solver2tactic(s)` in single-threaded mode (added in #9977).
Verified both `SINGLE_THREAD` and multi-threaded paths pass
`-fsyntax-only`.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Capture row as a pointer as lambda strips the reference and the vector was copied by value in lar_solver!
---------
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The `Ubuntu build - cmake - debugGcc` job was failing because the solver
could emit an unexpected `check-assignment` line before normal
satisfiability output. This change removes that stray output so debug
GCC runs no longer contaminate expected CLI/results streams.
- **Root cause**
- `src/math/lp/nra_solver.cpp` printed `check-assignment` from
`solver::check_assignment()` via `IF_VERBOSE(0, ...)`.
- Verbosity level `0` made this effectively unconditional in the failing
path, so debug builds could leak internal diagnostics into user-visible
output.
- **Change**
- Remove the `check-assignment` print from the exception path in
`lp::solver::check_assignment()`.
- Preserve all existing control flow and error handling; only the
unintended output side effect is removed.
- **Effect**
- Debug GCC CMake builds keep their normal `sat`/`unsat` output shape.
- Internal solver diagnostics no longer interfere with output-sensitive
CI checks.
```c++
catch (z3_exception &) {
statistics &st = m_imp->m_nla_core.lp_settings().stats().m_st;
m_imp->m_nlsat->collect_statistics(st);
if (m_imp->m_limit.is_canceled()) {
return l_undef;
}
else {
throw;
}
}
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
## Summary
Fixes the `iss-7027/small-30` snapshot regression (`Z3Prover/bench`
discussion #2705) **at its root**, instead of working around it by
retuning the LP heuristics.
- **Benchmark:** `inputs/issues/iss-7027/small-30.smt2` —
`(check-sat-using qe2)` over a single `(distinct ...)` of 33 mixed
Int/Real terms.
- The recorded oracle was `unknown`; current `master` produces
`timeout`.
## Root cause
`unknown`/`timeout` are both wrong here: the formula is a `distinct`
over 33 terms (free Int/Real constants plus the literals `0`/`1`), which
is **trivially `sat`** — there are infinitely many distinct reals.
The real bug is in the `qsat` tactic that backs `qe2`. Running
quantifier elimination on a **quantifier-free** formula has nothing to
eliminate, so `qsat` left an undecided residual goal and
`check-sat-using` reported `unknown`. This reproduces on any ground
formula with free variables, e.g.:
```
(declare-fun a () Int)(assert (> a 0))(check-sat-using qe2) ; -> unknown (should be sat)
```
For `small-30` the QE alternation additionally drove `theory_lra`
integer branch-and-bound down a non-terminating path, surfacing as a
`timeout` under the capture budget (the symptom the `random_hammers`
schedule change happened to expose).
## Fix
Under `check-sat` semantics, top-level free variables are implicitly
existentially quantified. So when the `qsat` input has no quantifiers,
decide satisfiability directly (route through the existing `qsat_sat`
path) instead of producing a residual goal. `qe2`/`qe` now return
`sat`/`unsat` for ground formulas.
QE of genuinely-quantified formulas is unchanged: `apply qe2` on a
quantified goal produces the same projected formula as before (verified
identical to `master`). Only the degenerate quantifier-free case is
affected.
This supersedes the previous approach in this PR (reverting the
`lp.random_hammers` default). That default is left **unchanged**
(`true`), preserving #9958's aggregate QF_LIA benefit. `small-30` now
returns `sat` in ~0.01s regardless of the heuristic schedule, because
the QE machinery no longer runs on this ground instance.
Two changes:
- `src/qe/qsat.cpp`: short-circuit quantifier-free input to the
satisfiability decision path.
- `Z3Prover/bench` `inputs/issues/iss-7027/small-30.expected.out`:
oracle updated `unknown` -> `sat` (to be committed alongside this fix).
## Validation
```
$ z3 small-30.smt2
sat # ~0.01s
$ echo '(declare-fun a () Int)(assert (> a 0))(check-sat-using qe2)' | z3 -in
sat
$ echo '(declare-fun a () Int)(assert (and (> a 0)(< a 0)))(check-sat-using qe2)' | z3 -in
unsat
```
Full unit-test suite (`test-z3 /a`) passes (92/92). Quantified `qe2`
round-trips (`apply qe2`) match `master` byte-for-byte.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
