From 37f1ac2e5d10585f2a12bbbc276dc181dd079964 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Fri, 10 Jul 2026 00:56:41 -0700 Subject: [PATCH] Fix MBQI model-construction regression on UFLIA (iss-5421) The term-enumeration change (#9908) added extra lambda definition equalities (val = term) to the auxiliary restriction context in restrict_sks_to_inst_set. These extra constraints over-constrain the auxiliary MBQI solver, causing model construction to fail (smt.mbqi :failed) and the solver to loop in final-check until timeout on otherwise-sat UFLIA problems. Restore the original restriction that constrains each skolem to one of its inverse values without asserting the lambda-definition equalities. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/smt/smt_model_finder.cpp | 19 ++++--------------- 1 file changed, 4 insertions(+), 15 deletions(-) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index c43028b40d..d9b9eb4bfd 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -2675,27 +2675,16 @@ namespace smt { obj_map const& inv = s->get_inv_map(); if (inv.empty()) continue; // nothing to do - expr_ref_vector eqs(m), defs(m); - - for (auto const& [val, term] : inv) { - if (val->get_sort() == sk->get_sort()) { - if (is_lambda(term)) { - eqs.push_back(m.mk_eq(sk, val)); - defs.push_back(m.mk_eq(val, term)); - } - else - eqs.push_back(m.mk_eq(sk, val)); - } + ptr_buffer eqs; + for (auto const& [val, _] : inv) { + if (val->get_sort() == sk->get_sort()) + eqs.push_back(m.mk_eq(sk, val)); } if (!eqs.empty()) { expr_ref new_cnstr(m); new_cnstr = m.mk_or(eqs); TRACE(model_finder, tout << "assert_restriction:\n" << mk_pp(new_cnstr, m) << "\n";); aux_ctx->assert_expr(new_cnstr); - for (auto def : defs) { - TRACE(model_finder, tout << "assert_def:\n" << mk_pp(def, m) << "\n";); - aux_ctx->assert_expr(def); - } asserted_something = true; } }