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 #4937

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-01-07 17:31:04 -08:00
parent 60ef60dff8
commit ac7d07ca58
2 changed files with 9 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/dyn_ack.cpp
View file

@ -80,8 +80,8 @@ namespace smt {
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 = ctx.mk_eq_atom(arg1, arg2);
app * neq = m.mk_not(eq); app_ref neq(m.mk_not(eq), m);
if (std::find(lits.begin(), lits.end(), neq) == lits.end()) { if (std::find(lits.begin(), lits.end(), neq.get()) == lits.end()) {
lits.push_back(neq); lits.push_back(neq);
prs.push_back(mk_hypothesis(m, eq, false, arg1, arg2)); prs.push_back(mk_hypothesis(m, eq, false, arg1, arg2));
} }
@ -398,7 +398,7 @@ namespace smt {
} }
literal dyn_ack_manager::mk_eq(expr * n1, expr * n2) { literal dyn_ack_manager::mk_eq(expr * n1, expr * n2) {
app_ref eq(m_context.mk_eq_atom(n1, n2), m); app_ref eq(m.mk_eq(n1, n2), m);
m_context.internalize(eq, true); m_context.internalize(eq, true);
literal l = m_context.get_literal(eq); literal l = m_context.get_literal(eq);
TRACE("dyn_ack", tout << "eq:\n" << mk_pp(eq, m) << "\nliteral: "; TRACE("dyn_ack", tout << "eq:\n" << mk_pp(eq, m) << "\nliteral: ";

9
src/smt/theory_seq.cpp
View file

@ -3028,9 +3028,11 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
if (n1 != n2 && m_util.is_seq(e1)) { if (n1 != n2 && m_util.is_seq(e1)) {
theory_var v1 = n1->get_th_var(get_id()); theory_var v1 = n1->get_th_var(get_id());
theory_var v2 = n2->get_th_var(get_id()); theory_var v2 = n2->get_th_var(get_id());
if (m_find.find(v1) == m_find.find(v2)) { if (v1 == null_theory_var || v2 == null_theory_var)
return; return;
} if (m_find.find(v1) == m_find.find(v2))
return;
m_find.merge(v1, v2); m_find.merge(v1, v2);
expr_ref o1(e1, m); expr_ref o1(e1, m);
expr_ref o2(e2, m); expr_ref o2(e2, m);
@ -3049,7 +3051,8 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
enode* n2 = get_enode(v2); enode* n2 = get_enode(v2);
expr_ref e1(n1->get_owner(), m); expr_ref e1(n1->get_owner(), m);
expr_ref e2(n2->get_owner(), m); expr_ref e2(n2->get_owner(), m);
SASSERT(n1->get_root() != n2->get_root()); if (n1->get_root() == n2->get_root())
return;
if (m_util.is_re(n1->get_owner())) { if (m_util.is_re(n1->get_owner())) {
m_regex.propagate_ne(e1, e2); m_regex.propagate_ne(e1, e2);
return; return;