From 2d327a008016330e3bd7074578f81c28873f4e79 Mon Sep 17 00:00:00 2001 From: "z3prover-ci-bot[bot]" <305651407+z3prover-ci-bot[bot]@users.noreply.github.com> Date: Sat, 1 Aug 2026 10:58:15 -0700 Subject: [PATCH] [fstar-build-fix] Fix nl-arith regression on F* obligation failedQueries-Pulse.Lib.PriorityQueue-3 (#10344) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary An F* proof build failed to discharge a proof obligation because z3 returned `unknown` instead of the expected `unsat`. This PR fixes an attributed nonlinear-arithmetic performance/completeness **regression** in z3 that caused the failure. - Originating F* build run: https://github.com/Z3Prover/z3/actions/runs/30685489878 - Failing query: `inputs/fstar-build-failures/run-30685489878/pulse/failedQueries-Pulse.Lib.PriorityQueue-3.smt2` (`Z3Prover/bench`) - Query label: `failedQueries-Pulse.Lib.PriorityQueue-3` - z3 ref under test: `1ba30df0282d2a673896afab1aa29de1caa32a10` - **Expected result:** `unsat` — **Observed on ref under test:** `unknown` (`:reason-unknown "canceled"`, i.e. the embedded `(set-option :rlimit 5000000)` budget was exhausted). The query embeds its own options (`smt.arith.solver=6`, `smt.mbqi=false`, `auto_config=false`, `rlimit=5000000`, ...); all runs below honor those embedded options. ## Root cause and attribution Bisecting `./z3` between a known-good baseline (`a05be8a29192d57c0b6596abf0e764fa924f6a6e`, which returns `unsat`) and the ref under test identified the first bad commit as: > **`90fe0aa0f32d4cf66f3503c249d1878a39c0cf3c` — "Imp fix (#10304)"** That commit adds `monomial_bounds::propagate_fixed_rows()` and calls it from `nla::core::propagate()`, gated by the new parameter `smt.arith.nl.propagate_fixed_rows` (default **true**). The routine scans **all** LP rows on **every** nonlinear-propagation call, and calls `lra.find_feasible_solution()` whenever anything is propagated. On this obligation that extra work consumes the `rlimit` budget before a proof is found, so a query that was previously `unsat` becomes `unknown` (`canceled`). This is a pure performance/completeness regression from a newly-added, parameter-gated heuristic — not a soundness issue in the query. ## Fix Default `smt.arith.nl.propagate_fixed_rows` to **false**, restoring the pre-#10304 behaviour. The heuristic and its code are left intact and remain available as opt-in via `smt.arith.nl.propagate_fixed_rows=true`, pending a more efficient implementation (e.g. not re-scanning every row on every propagation call). This is a one-line change in `src/params/smt_params_helper.pyg`; no solver check is weakened and the failing behaviour is not masked — the regressing heuristic is simply returned to being opt-in. ## Reproduction and validation All builds via `python3 scripts/mk_make.py && make -C build -j8` (CMake/Ninja unavailable in this environment; the Makefile build produces an equivalent binary). | z3 | `smt.arith.nl.propagate_fixed_rows` | Result | |---|---|---| | baseline `a05be8a` | (n/a, pre-feature) | `unsat` | | ref under test `1ba30df` | true (default) | `unknown` (canceled) | | ref under test `1ba30df` | false (override) | `unsat` | | **patched `1ba30df` (this PR)** | false (new default) | **`unsat`** | Before the fix the query reproduced the `unknown`/`canceled` failure; after the fix the patched binary returns the expected `unsat` with the query's embedded options unchanged. ## Notes / uncertainty This change restores correctness-preserving behaviour by disabling an optional heuristic by default rather than reworking its cost model. A follow-up could re-enable the heuristic once its per-propagation cost is bounded (e.g. only scanning rows touched since the last call). Created as a **draft** for maintainer review. > [!WARNING] >
> Firewall blocked 1 domain > > The following domain was blocked by the firewall during workflow execution: > > - `pypi.org` >> To allow these domains, add them to the `network.allowed` list in your workflow frontmatter: > > ```yaml > network: > allowed: > - defaults > - "pypi.org" > ``` > > See [Network Configuration](https://github.github.com/gh-aw/reference/network/) for more information. > >
> Generated by [Fix a Z3 failure on an F* proof obligation](https://github.com/Z3Prover/bench/actions/runs/30692520945) · 398.4 AIC · ⌖ 21.5 AIC · ⊞ 9.4K · [◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+fstar-build-fixer%22&type=pullrequests) Co-authored-by: z3prover-ci-bot[bot] <305651407+z3prover-ci-bot[bot]@users.noreply.github.com> Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/params/smt_params_helper.pyg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg index 3c04bc5a43..9753e42072 100644 --- a/src/params/smt_params_helper.pyg +++ b/src/params/smt_params_helper.pyg @@ -101,7 +101,7 @@ def_module_params(module_name='smt', ('arith.nl.delay', UINT, 10, 'number of calls to final check before invoking bounded nlsat check'), ('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'), ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'), - ('arith.nl.propagate_fixed_rows', BOOL, True, 'scan LP rows for fixed variables'), + ('arith.nl.propagate_fixed_rows', BOOL, False, 'scan LP rows for fixed variables'), ('arith.nl.optimize_bounds_lp_max_vars', UINT, 120, 'skip LP-based nonlinear bounds optimization when the number of candidate monomial variables exceeds this threshold (0 = unlimited)'), ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'), ('arith.nl.log', BOOL, False, 'Log lemmas sent to nra solver'),