mirror of
https://github.com/Z3Prover/z3
synced 2026-07-15 03:25:43 +00:00
6a62a53181
## 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> |
||
|---|---|---|
| .. | ||
| ackermannization | ||
| api | ||
| ast | ||
| cmd_context | ||
| math | ||
| model | ||
| muz | ||
| nlsat | ||
| opt | ||
| params | ||
| parsers | ||
| qe | ||
| sat | ||
| shell | ||
| smt | ||
| solver | ||
| tactic | ||
| test | ||
| util | ||
| CMakeLists.txt | ||