mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-07 06:28:18 +00:00
Code Activity

Fix 10388 (#10418)

Browse source 
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a8f87ede-b718-4fe9-9839-cc9eaaf9c3a7
This commit is contained in:
Nikolaj Bjorner 2026-08-05 19:27:03 -07:00 • committed by GitHub
parent ce9d276294
commit 9167020d83
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/smt_conflict_resolution.cpp
View file

@ -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 {
}
}

3
src/smt/smt_context.cpp
View file

@ -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);