From f5a28aacf5dd9c305609199c4fb90e928acbe618 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Thu, 25 Jun 2026 02:17:13 -0700 Subject: [PATCH] Fix MBQI ho_var term-enumeration timeout regression (iss-6174/small.smt2) Commit 6fd303c4b ("set the auf flag to false in all cases") additionally added two Boolean productions to the ho_var instantiation-set enumeration in smt_model_finder.cpp: tn.add_production(m.mk_true()); tn.add_production(m.mk_false()); For benchmarks whose universally-quantified array variable has a deeply nested array sort that unfolds to a Bool target sort (e.g. the forall over r : (Array (Array Bool Bool) (Array Bool Bool)) in iss-6174/small.smt2), these extra Bool leaves combine combinatorially with the select/store/eq operators in term_enumeration. enum_terms then blows up and MBQI hangs: the third check-sat, which previously returned quickly, now times out at -T:20 (and even -T:60). The pre-existing max_count=20 bound limits how many terms are inserted but not the enumerator's internal work. Remove the two auxiliary Boolean productions. The commit's titular change (setting m_is_auf = false in all cases) is benign for this benchmark and is preserved; only the enumeration-blowup lines are dropped. After the fix the benchmark returns "sat sat sat" with no timeout, and the third query's model passes model_validate=true. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/smt/smt_model_finder.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 6ef1e55c6e..1dc63ff2a4 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -1413,8 +1413,6 @@ namespace smt { // add other possible relevant functions such as equality over srt, Boolean operators ast_mark visited; - tn.add_production(m.mk_true()); - tn.add_production(m.mk_false()); for (enode *n : ctx->enodes()) { if (!ctx->is_relevant(n)) continue;