Repository navigation
Tags
Tags
Remove timing-out arithmetic alias SAT control Retain arithmetic alias proof checks and remove the SAT control that exceeds its solver timeout. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 7c1bd3c9-2f54-4052-9647-f97c0815bc96
Remove timing-out arithmetic alias SAT control Retain arithmetic alias proof checks and remove the SAT control that exceeds its solver timeout. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 7c1bd3c9-2f54-4052-9647-f97c0815bc96
Keep finite-set cardinality state consistent across backtracking (Z3P… …rover#11440) An unrelated positive finite-set cardinality constraint could make satisfiable transcendental arithmetic return `unsat`. Backtracking reset the solver’s completion flag while retaining its exhausted Boolean subsolver, allowing a subsequent run to emit an incorrect zero-cardinality equation. - **Solver lifecycle:** Reset the completion flag when the associated subsolver is cleared; remove its independent trail. - **Regression:** Check the reported formula in default and model-validation modes. ```smt2 (assert (>= (+ (sin x) (exp x FB1A )) 4.0)) (assert (>= (+ (sin y) (exp y)) 4.0)) (assert (= (set.size S) 1)) (check-sat) ; sat ``` <!-- START COPILOT CODING AGENT SUFFIX --> - Fixes Z3Prover#11431 --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Relnotes (Z3Prover#11174) Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Record merged smart-constructor baseline for regex study Rebase the unchanged study controls onto master after PR Z3Prover#10926. Identify the merged union-fix ancestor and retain the original campaign source pin under bisim-study-pre-smart-20260925. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 2b2c550e-6679-4743-8837-5e52092a1d81
opt: return arithmetic maximization results explicitly (Z3Prover#10921) ## Summary Follow up on Z3Prover#10914 by making the arithmetic-side result self-contained. - Return `opt_solver::maximize_result { bound_valid, hint, hint_status }` from `maximize_objective` instead of a Boolean plus mutable last-call fields/getters. - Update `geometric_search` and `maximize_objective_isolated` to read the returned record. Keep the blocker output parameter and existing objective/model storage. - Preserve acceptance separately from validation: the existing no-model path still returns `bound_valid=true` with `hint_status=l_undef`. The original hint is captured before validation, at the same point as the old field assignment. - Add an `opt_bounds` case checking exact hint values, acceptance/status, blockers, saved objective values, and that a later objective does not overwrite an earlier result. This is an internal representation refactor, not a new algorithm or a public C API change. Solver calls, model/bound updates, callbacks, budgets, and fallback decisions are unchanged. ## Validation Based on current master `b7f2ccbc9`, rebuilt before saving the comparison binary. - Release/debug builds of `z3` and `test-z3` passed; release `libz3` also rebuilt. - Full unit suite (`test-z3 /a /j:4`): **108 passed, 0 failed** in each build. - Explicit optimization suites (`opt_bounds opt_nlsat opt_pareto opt_value`): **4 passed, 0 failed** in each build, including the new per-call result test. - Existing z3test optimization regressions, selected by optimization commands or `opt*` names and run with `model_validate=true`: **83 passed, 0 failed** in each build. Outputs are byte-identical to expected files and the saved master binary. - opt_z3 LRA/NRA harness: **23/23 records unchanged**, excluding elapsed time (21 PASS, the same 2 existing BOUNDS results). - Additional disabled-nlsat and low-resource runs: **46/46** base/refactor pairs have identical exit codes, stdout, and stderr. Used `rlimit=5000 opt.optsmt_nlsat=false opt.optsmt_bisect_rounds=8`, and separately `rlimit=1000`. - CLI solving/help, local Python bindings, and `git diff --check` passed. No expected answers were changed. --------- Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 855fb1bb-02b4-48ba-9f8a-84eaf9aafc3d
Enforce the quantified regex regression resource budget The test calls solver::check_sat directly, so setting the rlimit parameter does not install the API resource scope. The union normal form changes the quantified search path and exposed this accidentally unbounded test, eventually overflowing signed 24-bit theory-variable storage. Install the intended scoped_rlimit instead; retain both union constructor fixes and permit unknown as the crash-safety test originally intended. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 2b2c550e-6679-4743-8837-5e52092a1d81
PreviousNext