From ba2f587c261096e5f33ee6c9f2e9633c3298a964 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 11 Feb 2020 18:39:32 -0800 Subject: [PATCH] rm eq Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 150b6c6df..45fff2d4e 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1093,6 +1093,7 @@ public: // this step ensures that a shared enode is attached // with the ite expression. else if (m.is_ite(lhs) || m.is_ite(rhs)) { + // std::cout << "eq\n"; m_arith_eq_adapter.mk_axioms(n1, n2); } }