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

add guard for eq adapter

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-06-13 16:39:53 -07:00
parent ac00306355
commit cc4ac0e65a
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_lra.cpp
View file

@ -1017,12 +1017,16 @@ public:
} }
void internalize_eq_eh(app * atom, bool_var) { void internalize_eq_eh(app * atom, bool_var) {
if (!ctx().get_fparams().m_arith_eager_eq_axioms)
return;
expr* lhs = nullptr, *rhs = nullptr; expr* lhs = nullptr, *rhs = nullptr;
VERIFY(m.is_eq(atom, lhs, rhs)); VERIFY(m.is_eq(atom, lhs, rhs));
enode * n1 = get_enode(lhs); enode * n1 = get_enode(lhs);
enode * n2 = get_enode(rhs); enode * n2 = get_enode(rhs);
TRACE("arith_verbose", tout << mk_pp(atom, m) << " " << is_arith(n1) << " " << is_arith(n2) << "\n";);
if (is_arith(n1) && is_arith(n2) && n1 != n2) if (is_arith(n1) && is_arith(n2) &&
n1->get_th_var(get_id()) != null_theory_var &&
n2->get_th_var(get_id()) != null_theory_var && n1 != n2)
m_arith_eq_adapter.mk_axioms(n1, n2); m_arith_eq_adapter.mk_axioms(n1, n2);
} }