From 22c779c77c79e327bc96b17eff72c8b4cff347f1 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Tue, 7 Jul 2026 13:02:37 -0700 Subject: [PATCH] [snapshot-regression-fix] Fix elim_uncnstr disabled by manager-wide has_type_vars() flag (iss-6260/small-2) (#10063) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary Fixes a completeness regression where `elim_uncnstr` was silently disabled for ordinary (non-polymorphic) goals, detected by the `snapshot-regression` corpus. - **Originating discussion:** https://github.com/Z3Prover/bench/discussions/3054 - **Benchmark:** `iss-6260/small-2.smt2` (corpus `Z3Prover/bench`, `inputs/issues/iss-6260/`) - **Divergence:** recorded oracle `sat` → current z3 produces `unknown` ### Divergence diff ```diff --- small-2.expected.out (expected) +++ produced (current z3) @@ -1,3 +1,3 @@ -sat +unknown (error "line 17 column 0: unexpected character") (error "line 17 column 1: unexpected character") ``` (The `(error ...)` lines are expected: the benchmark contains a stray ```` ``` ```` fence on line 17. Only the `sat` → `unknown` change is the regression.) ## Root cause `git bisect` over the regression window pins the flip to commit `208cc5686` ("fix build"), which added `|| m().has_type_vars()` to the `elim_uncnstr_tactic` guard and an equivalent `if (m.has_type_vars()) return;` to the `elim_unconstrained` simplifier. `ast_manager::has_type_vars()` is a **manager-wide, sticky** flag: it is set to `true` as soon as *any* type variable is created, and is never reset. In particular `finite_set_decl_plugin::init()` creates type variables `A`/`B` to define its polymorphic signatures. Those type variables never occur in the user's assertions, but once the finite_set plugin is initialized — which happens while processing this benchmark — the flag is globally `true` (confirmed by instrumenting `mk_type_var`: the only type vars created for this benchmark are the finite_set signature vars `A` and `B`). As a result `elim_uncnstr` bails out for goals that contain **no** polymorphic terms at all, i.e. it is effectively disabled. Unconstrained subterms that used to be eliminated now reach the theory solvers. For this benchmark the (single) assertion is `(not (xor (>= x 0) (>= x1 0) (>= x 0) x4 (str.contains ...)))`. The duplicated `(>= x 0)` cancels (`a xor a = false`), and the free Boolean `x4` can fix the parity regardless of the value of the `str.contains` term, so the goal is trivially `sat`. That `str.contains`/`str.replace_re` subterm is unconstrained and was previously removed by `elim_uncnstr`; without that elimination it reaches `theory_seq`, which marks `str.replace_re` as unhandled and gives up in `final_check` → `unknown` (`incomplete (theory seq)`). ## Fix Make the guard precise. Keep `has_type_vars()` as a cheap pre-filter (matching existing usage in `ast_translation.cpp` and `ast_manager::has_type_var`), but only bail out when the goal / asserted formulas **actually** contain type-variable typed terms, using the existing `polymorphism::util::has_type_vars(expr*)`. This preserves the polymorphism crash-protection (goals with genuine type-variable terms still skip `elim_uncnstr`) while restoring `elim_uncnstr` for the vast majority of goals that merely triggered a polymorphic-plugin initialization. Both twin guards (the `elim_uncnstr` tactic and the `elim_unconstrained` simplifier) are fixed consistently. ## Validation Built this checkout and re-ran the benchmark (step 5 of the fixer workflow): - `./configure && make -C build -j$(nproc)` — Z3 version 4.17.0. - Unpatched master reproduced the divergence: `z3 -T:20 iss-6260/small-2.smt2` → `unknown`. - After the fix, `z3 -T:20 inputs/issues/iss-6260/small-2.smt2` produces **exactly** the recorded oracle: ``` sat (error "line 17 column 0: unexpected character") (error "line 17 column 1: unexpected character") (error "line 17 column 2: unexpected character") ``` - Regression sanity checks: sibling `iss-6260/small.smt2` unchanged (`sat`); plain arithmetic unconstrained goals unchanged; polymorphic goals with genuine type-variable terms (including `declare-type-var` and forcing `(check-sat-using (then elim-uncnstr smt))`) still solve without crashing — the guard still fires for those. Opened as a **draft** for human review. > Generated by [Fix a Z3 snapshot-regression divergence](https://github.com/Z3Prover/bench/actions/runs/28844840657) · 861.2 AIC · ⌖ 45.8 AIC · ⊞ 8.9K · [◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+snapshot-regression-fixer%22&type=pullrequests) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/ast/simplifiers/elim_unconstrained.cpp | 15 +++++++++++++-- src/tactic/core/elim_uncnstr_tactic.cpp | 18 +++++++++++++++++- 2 files changed, 30 insertions(+), 3 deletions(-) diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp index 120fe06729..c7742861b1 100644 --- a/src/ast/simplifiers/elim_unconstrained.cpp +++ b/src/ast/simplifiers/elim_unconstrained.cpp @@ -116,6 +116,7 @@ eliminate: #include "ast/ast_ll_pp.h" #include "ast/ast_pp.h" #include "ast/recfun_decl_plugin.h" +#include "ast/polymorphism_util.h" #include "ast/simplifiers/elim_unconstrained.h" elim_unconstrained::elim_unconstrained(ast_manager& m, dependent_expr_state& fmls) : @@ -425,8 +426,18 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector< void elim_unconstrained::reduce() { if (!m_config.m_enabled) return; - if (m.has_type_vars()) - return; + // has_type_vars() is a manager-wide flag that is set as soon as any type variable is + // created, including the ones used to define polymorphic signatures of builtin plugins + // (e.g. finite_set) that never occur in the asserted formulas. Only bail out when the + // formulas actually contain type-variable typed terms, which this simplifier cannot invert. + if (m.has_type_vars()) { + polymorphism::util u(m); + for (unsigned i : indices()) { + auto [f, p, d] = m_fmls[i](); + if (u.has_type_vars(f)) + return; + } + } generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained"); m_inverter.set_model_converter(mc.get()); m_created_compound = true; diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index a0eaeead94..7aecd4d505 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -27,6 +27,7 @@ Notes: #include "ast/datatype_decl_plugin.h" #include "ast/seq_decl_plugin.h" #include "ast/for_each_expr.h" +#include "ast/polymorphism_util.h" #include "tactic/core/collect_occs.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_ll_pp.h" @@ -936,6 +937,21 @@ class elim_uncnstr_tactic : public tactic { m_rw = alloc(rw, m(), produce_proofs, m_vars, m_nonvars, m_disabled, m_mc.get(), m_max_memory, m_max_steps); } + // The manager-wide has_type_vars() flag is a coarse over-approximation: it becomes + // true as soon as any type variable is created, including the type variables used to + // define the polymorphic signatures of builtin plugins (e.g. finite_set). Those never + // occur in the actual goal, so relying on the global flag needlessly disables this + // tactic. Check whether the goal itself contains type-variable typed terms instead. + bool goal_has_type_vars(goal_ref const & g) { + if (!m().has_type_vars()) + return false; + polymorphism::util u(m()); + for (unsigned i = 0; i < g->size(); ++i) + if (u.has_type_vars(g->form(i))) + return true; + return false; + } + void run(goal_ref const & g, goal_ref_buffer & result) { bool produce_proofs = g->proofs_enabled(); TRACE(goal, g->display(tout);); @@ -945,7 +961,7 @@ class elim_uncnstr_tactic : public tactic { collect_occs p; p(*g, m_vars); disable_quantified(g); - if (m_vars.empty() || recfun::util(m()).has_rec_defs() || m().has_type_vars()) { + if (m_vars.empty() || recfun::util(m()).has_rec_defs() || goal_has_type_vars(g)) { result.push_back(g.get()); // did not increase depth since it didn't do anything. return;