mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 04:41:21 +00:00
Code Activity

fix #4933

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-01-08 10:57:55 -08:00
parent 0173359a50
commit c36355c1e5
2 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/dyn_ack.cpp
View file

@ -79,7 +79,7 @@ namespace smt {
expr * arg1 = m_app1->get_arg(i); expr * arg1 = m_app1->get_arg(i);
expr * arg2 = m_app2->get_arg(i); expr * arg2 = m_app2->get_arg(i);
if (arg1 != arg2) { if (arg1 != arg2) {
app * eq = ctx.mk_eq_atom(arg1, arg2); app * eq = m.mk_eq(arg1, arg2);
app_ref neq(m.mk_not(eq), m); app_ref neq(m.mk_not(eq), m);
if (std::find(lits.begin(), lits.end(), neq.get()) == lits.end()) { if (std::find(lits.begin(), lits.end(), neq.get()) == lits.end()) {
lits.push_back(neq); lits.push_back(neq);
@ -89,7 +89,7 @@ namespace smt {
} }
proof * antecedents[2]; proof * antecedents[2];
antecedents[0] = m.mk_congruence(m_app1, m_app2, prs.size(), prs.c_ptr()); antecedents[0] = m.mk_congruence(m_app1, m_app2, prs.size(), prs.c_ptr());
app * eq = ctx.mk_eq_atom(m_app1, m_app2); app * eq = m.mk_eq(m_app1, m_app2);
antecedents[1] = mk_hypothesis(m, eq, true, m_app1, m_app2); antecedents[1] = mk_hypothesis(m, eq, true, m_app1, m_app2);
proof * false_pr = m.mk_unit_resolution(2, antecedents); proof * false_pr = m.mk_unit_resolution(2, antecedents);
lits.push_back(eq); lits.push_back(eq);
@ -485,9 +485,9 @@ namespace smt {
justification * js = nullptr; justification * js = nullptr;
if (m.proofs_enabled()) { if (m.proofs_enabled()) {
js = alloc(dyn_ack_eq_justification, n1, n2, r, js = alloc(dyn_ack_eq_justification, n1, n2, r,
to_app(ctx.bool_var2expr(eq1.var())), m.mk_eq(n1, r),
to_app(ctx.bool_var2expr(eq2.var())), m.mk_eq(n2, r),
to_app(ctx.bool_var2expr(eq3.var()))); m.mk_eq(n1, n2));
} }
clause * cls = ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_TH_LEMMA, del_eh); clause * cls = ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_TH_LEMMA, del_eh);
if (!cls) { if (!cls) {

4
src/smt/smt_conflict_resolution.cpp
View file

@ -1256,8 +1256,7 @@ namespace smt {
void conflict_resolution::mk_conflict_proof(b_justification conflict, literal not_l) { void conflict_resolution::mk_conflict_proof(b_justification conflict, literal not_l) {
SASSERT(conflict.get_kind() != b_justification::BIN_CLAUSE); SASSERT(conflict.get_kind() != b_justification::BIN_CLAUSE);
SASSERT(conflict.get_kind() != b_justification::AXIOM); SASSERT(not_l == null_literal || conflict.get_kind() == b_justification::AXIOM || conflict.get_kind() == b_justification::JUSTIFICATION);
SASSERT(not_l == null_literal || conflict.get_kind() == b_justification::JUSTIFICATION);
TRACE("mk_conflict_proof", m_ctx.display_literals(tout << "lemma literals:", m_lemma) << "\n";); TRACE("mk_conflict_proof", m_ctx.display_literals(tout << "lemma literals:", m_lemma) << "\n";);
reset(); reset();
@ -1350,6 +1349,7 @@ namespace smt {
m_lemma_proof = pr; m_lemma_proof = pr;
else else
m_lemma_proof = m.mk_lemma(pr, fact); m_lemma_proof = m.mk_lemma(pr, fact);
TRACE("mk_conflict_proof", tout << mk_pp(m_lemma_proof, m) << "\n";);
m_new_proofs.reset(); m_new_proofs.reset();
reset(); reset();
} }