From d1170d19bd90e9ffa89dfd4063c488edd00522a7 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Wed, 24 Jun 2026 10:58:32 -0700 Subject: [PATCH] [snapshot-regression-fix] Bound ho_var term enumeration to fix MBQI timeout regression (iss-5753/small-3.smt2) (#9939) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary Fixes a Z3 snapshot-regression divergence tracked in Z3Prover/bench discussion https://github.com/Z3Prover/bench/discussions/2662. - **Benchmark:** `iss-5753/small-3.smt2` (Z3Prover/bench corpus, original issue z3#5753) - **Regression:** recorded oracle `unsat` (captured 2026-06-05) → current `master` produces `timeout` at `-T:20` - **bench workflow run:** https://github.com/Z3Prover/bench/actions/runs/28078176175 ### Divergence ```diff --- small-3.expected.out (expected) +++ produced (current z3) @@ -1 +1 @@ -unsat +timeout ``` The answer `unsat` is still correct — z3 simply can no longer prove it within the budget. This is a **performance regression**, not a wrong/unsound result. ## Root cause The benchmark is a quantified Array/Real/Int problem solved via MBQI. The model finder's quantifier analyzer (`src/smt/smt_model_finder.cpp`) now creates a `ho_var` qinfo for **array-sorted quantified variables used as terms** (the new higher-order term-enumeration path introduced in #9908, "Term enumeration", commit `5699142f5`). Before that commit such an occurrence set `m_info->m_is_auf = false` (a safe fallback that left no extra instantiation hints), which is the behaviour that was active when the `unsat` oracle was captured. `ho_var::populate_inst_sets` builds instantiation candidates with: ```cpp for (auto t : tn.enum_terms(srt)) { ... S->insert(t, generation); } ``` `term_enumeration::enum_terms` is a **lazy, increasing-cost generator with no inherent bound** (see `ast/rewriter/term_enumeration.h`). For this benchmark the relevant array sort `(Array Int (Array Int Real))` has many array-valued uninterpreted productions (`tptpummul`, `trans`, `inv`, ...), so iterating the generator to exhaustion inserts an explosively large number of terms into the instantiation set, blowing up MBQI instantiation and exhausting the 20s budget. Confirmed empirically: running the benchmark with `-v:3` shows `ho_var::populate_inst_sets: 622 (Array Int (Array Int Real))`, i.e. this exact path fires for the divergent benchmark. Notably, the original commit `5699142f5` declared `unsigned max_count = 20;` for this very loop but **never applied it**, and that dead variable was subsequently removed — leaving the enumeration completely unbounded. ## Fix Restore the intended bound so at most 20 of the cheapest enumerated terms are added to the instantiation set: ```cpp unsigned max_count = 20; for (auto t : tn.enum_terms(srt)) { if (max_count == 0) break; --max_count; ... S->insert(t, generation); } ``` This is sound (instantiation only ever adds valid ground instances of the quantified formula) and is strictly more information than the pre-#9908 baseline (which added no `ho_var` terms at all), so it does not regress problems the feature was meant to help. The change is confined to a single loop in `src/smt/smt_model_finder.cpp`. ## Validation Built the checkout in Release mode and re-ran the failing benchmark with the same options the snapshot harness uses: ``` $ build/z3 -T:20 inputs/issues/iss-5753/small-3.smt2 unsat # was: timeout real 0m0.120s ``` The combined output now matches the recorded `small-3.expected.out` oracle **byte-for-byte** (`unsat\n`). A smoke run over a sample of other corpus benchmarks showed no crashes or new divergences, and a basic `(check-sat)/(get-model)` sanity check still works. --- This PR is opened as a **draft** for human review by the automated snapshot-regression fixer. 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/28078343154) · 2.8K AIC · ⌖ 150.7 AIC · ⊞ 39K · [◷](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/smt/smt_model_finder.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index b5d2ee7719..9483faecff 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -1435,7 +1435,11 @@ namespace smt { } } + unsigned max_count = 20; for (auto t : tn.enum_terms(srt)) { + if (max_count == 0) + break; + --max_count; unsigned generation = 0; // todo - inherited from sub-term of t? TRACE(model_finder, tout << "ho_var: adding term " << mk_ismt2_pp(t, m) << " to instantiation set of S" << std::endl;);