From 3d29d816075d6358dc5fd9e7d544dbbe5e0e554d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2026 20:32:04 -0700 Subject: [PATCH] Fix TPTP polymorphism crashes in final-check and model checking Root-caused and fixed 261 debug-assertion crashes found by running Z3 across the TPTP benchmarks (-tptp -T:5 model_validate=true): 1. theory_polymorphism::final_check_eh returned FC_DONE after assigning the negation of its (already-true) theory assumption, which creates a conflict. Returning FC_DONE reported l_true while the context was inconsistent, tripping SASSERT(status != l_true || !inconsistent()) in context::restart. Return FC_CONTINUE so conflict resolution turns it into l_false and the normal research loop runs. 2. model_evaluator::get_macro, polymorphic branch: def = subst(def) assigned an expr_ref temporary to a raw expr*&; the temporary freed the freshly substituted term, leaving def dangling (use-after-free during model evaluation). Pin the substituted def in m_pinned, as the as-array path already does. 3. smt_model_checker::add_instance: relax stale SASSERT(!m.is_model_value(sk_term)); get_inv may legitimately return a model value in polymorphic settings, already handled downstream by get_type_compatible_term. Unit tests: 92 passed, 0 failed. All 261 assertion crashes resolved; the 3 remaining files are controlled ERR_PARSER (exit 103) rejections. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/model/model_evaluator.cpp | 4 +++- src/smt/smt_model_checker.cpp | 3 ++- src/smt/theory_polymorphism.h | 12 +++++++++++- 3 files changed, 16 insertions(+), 3 deletions(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 8422006677..840c86730e 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -404,7 +404,9 @@ struct evaluator_cfg : public default_rewriter_cfg { polymorphism::substitution subst(m); polymorphism::util util(m); util.unify(f, m.poly_root(f), subst); - def = subst(def); + expr_ref d = subst(def); + m_pinned.push_back(d); + def = d; SASSERT(def != nullptr); } diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 64dc77eb59..255254fe41 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -222,7 +222,8 @@ namespace smt { expr * sk_term = m_model_finder.get_inv(q, i, sk_value, *cex, sk_term_gen); if (sk_term != nullptr) { TRACE(model_checker, tout << "Found inverse " << mk_pp(sk_term, m) << "\n";); - SASSERT(!m.is_model_value(sk_term)); + // get_inv may return a model value in polymorphic settings; + // this is handled downstream by get_type_compatible_term. max_generation = std::max(sk_term_gen, max_generation); sk_value = sk_term; } diff --git a/src/smt/theory_polymorphism.h b/src/smt/theory_polymorphism.h index 613c1a8dd5..95e0afc136 100644 --- a/src/smt/theory_polymorphism.h +++ b/src/smt/theory_polymorphism.h @@ -67,8 +67,18 @@ namespace smt { } final_check_status final_check_eh(unsigned) override { - if (m_inst.pending()) + if (m_inst.pending()) { + // There are still polymorphic axioms to instantiate. Force the + // solver to fail under the theory assumption so that a new + // research round (see should_research) can assert the new + // instances. Assigning the negation of the (already true) + // assumption creates a conflict, so we must return FC_CONTINUE + // to let conflict resolution turn it into l_false; returning + // FC_DONE here would report l_true while the context is + // inconsistent, violating a core search invariant. ctx.assign(~mk_literal(m_assumption), nullptr); + return FC_CONTINUE; + } return FC_DONE; }