mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

fix #4952

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-01-20 00:49:28 -08:00
parent 80f429c3fb
commit 3a2ed691f8
1 changed files with 12 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/smt/dyn_ack.cpp
View file

@ -73,11 +73,11 @@ namespace smt {
ast_manager & m = cr.get_manager();
context & ctx = cr.get_context();
unsigned num_args = m_app1->get_num_args();
ptr_buffer<proof> prs;
ptr_buffer<expr> lits;
proof_ref_vector prs(m);
expr_ref_vector lits(m);
for (unsigned i = 0; i < num_args; i++) {
expr * arg1 = m_app1->get_arg(i);
expr * arg2 = m_app2->get_arg(i);
expr * arg1 = m_app1->get_arg(i);
expr * arg2 = m_app2->get_arg(i);
if (arg1 != arg2) {
app * eq = m.mk_eq(arg1, arg2);
app_ref neq(m.mk_not(eq), m);
@ -87,16 +87,16 @@ namespace smt {
}
}
}
proof * antecedents[2];
antecedents[0] = m.mk_congruence(m_app1, m_app2, prs.size(), prs.c_ptr());
app * eq = m.mk_eq(m_app1, m_app2);
antecedents[1] = mk_hypothesis(m, eq, true, m_app1, m_app2);
proof * false_pr = m.mk_unit_resolution(2, antecedents);
app_ref eq(m.mk_eq(m_app1, m_app2), m);
proof_ref a1(m.mk_congruence(m_app1, m_app2, prs.size(), prs.c_ptr()), m);
proof_ref a2(mk_hypothesis(m, eq, true, m_app1, m_app2), m);
proof * antecedents[2] = { a1.get(), a2.get() };
proof_ref false_pr(m.mk_unit_resolution(2, antecedents), m);
lits.push_back(eq);
SASSERT(lits.size() >= 2);
app * lemma = m.mk_or(lits.size(), lits.c_ptr());
TRACE("dyn_ack", tout << mk_pp(lemma, m) << "\n";);
TRACE("dyn_ack", tout << mk_pp(false_pr, m) << "\n";);
app_ref lemma(m.mk_or(lits), m);
TRACE("dyn_ack", tout << lemma << "\n";);
TRACE("dyn_ack", tout << false_pr << "\n";);
return m.mk_lemma(false_pr, lemma);
}