mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
Can's fix to relevancy propagation
This commit is contained in:
parent
89ed4d6c8b
commit
8c5abdf818
|
@ -425,6 +425,9 @@ namespace smt {
|
|||
lits.push_back(mk_eq(n1, n2));
|
||||
clause_del_eh * del_eh = alloc(dyn_ack_clause_del_eh, *this);
|
||||
|
||||
for (auto lit : lits)
|
||||
m_context.mark_as_relevant(lit);
|
||||
|
||||
justification * js = nullptr;
|
||||
if (m.proofs_enabled())
|
||||
js = alloc(dyn_ack_cc_justification, n1, n2);
|
||||
|
@ -484,6 +487,9 @@ namespace smt {
|
|||
m.mk_eq(n2, r),
|
||||
m.mk_eq(n1, n2));
|
||||
}
|
||||
ctx.mark_as_relevant(eq1);
|
||||
ctx.mark_as_relevant(eq2);
|
||||
ctx.mark_as_relevant(eq3);
|
||||
clause * cls = ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, del_eh);
|
||||
if (!cls) {
|
||||
dealloc(del_eh);
|
||||
|
|
|
@ -2321,6 +2321,8 @@ namespace smt {
|
|||
});
|
||||
literal l(v, sign);
|
||||
cls->set_literal(j, l);
|
||||
if (cls->get_kind() == CLS_TH_LEMMA)
|
||||
mark_as_relevant(l);
|
||||
}
|
||||
SASSERT(ilvl <= m_scope_lvl);
|
||||
int w1_idx = select_watch_lit(cls, 0);
|
||||
|
@ -2349,6 +2351,10 @@ namespace smt {
|
|||
SASSERT(!cls->reinternalize_atoms());
|
||||
literal l1 = cls->get_literal(0);
|
||||
literal l2 = cls->get_literal(1);
|
||||
if (cls->get_kind() == CLS_TH_LEMMA) {
|
||||
mark_as_relevant(l1);
|
||||
mark_as_relevant(l2);
|
||||
}
|
||||
if (get_assignment(l1) == l_false && is_empty_clause(cls)) {
|
||||
set_conflict(b_justification(cls));
|
||||
keep = true;
|
||||
|
|
Loading…
Reference in a new issue