Distilled companion to d5-two-var-square.smt2: x.x in (Sigma* "a" Sigma*)
with |x|=1 is sat (x="a"), but smt.string_solver=nseq returns unsat.
Trigger = regex membership over a str.++ of variable terms + an exact length
(str.len = k, or a word equation forcing lengths); default/seq/z3str3 are
correct. nseq is a c3-branch-only solver; master is unaffected.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
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>
