From cc4ac0e65a2713b366cca02431840117904672c4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 13 Jun 2023 16:39:53 -0700 Subject: [PATCH] add guard for eq adapter --- src/smt/theory_lra.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index c6bd12f03..8bb80db58 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1017,12 +1017,16 @@ public: } void internalize_eq_eh(app * atom, bool_var) { + if (!ctx().get_fparams().m_arith_eager_eq_axioms) + return; expr* lhs = nullptr, *rhs = nullptr; VERIFY(m.is_eq(atom, lhs, rhs)); enode * n1 = get_enode(lhs); 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); }