From 9167020d833576d52bc65552652b0c95f9f4f6a0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Aug 2026 19:27:03 -0700 Subject: [PATCH] Fix 10388 (#10418) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: a8f87ede-b718-4fe9-9839-cc9eaaf9c3a7 --- src/smt/smt_conflict_resolution.cpp | 3 ++- src/smt/smt_context.cpp | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index fae8ee9720..ea8f21be5d 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -1044,6 +1044,8 @@ namespace smt { tout << l.index() << " " << true_literal.index() << " " << false_literal.index() << " "; m_ctx.display_literal(tout, l); tout << " --->\n"; tout << mk_ll_pp(l_exr, m);); + if (prs.size() > 2 && !m.is_or(m.get_fact(prs[0]))) + throw default_exception("malformed clause proof in conflict resolution"); pr = m.mk_unit_resolution(prs.size(), prs.data(), l_exr); m_new_proofs.push_back(pr); return pr; @@ -1486,4 +1488,3 @@ namespace smt { } } - diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index b8e572513a..79a8363051 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3849,7 +3849,8 @@ namespace smt { } for (auto const& clause : clauses) init_clause(clause); r = search(); - r = mk_unsat_core(r); + r = mk_unsat_core(r); + reset_tmp_clauses(); } while (should_research(r)); r = check_finalize(r);