From e4e1d6148c336a5d65337e27e04bfda85b528d9d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 26 Sep 2023 20:14:42 -0700 Subject: [PATCH] port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 518cffe25..c0cfe3876 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1799,11 +1799,10 @@ public: bool check_idiv_bounds() { if (!m_nla) return true; - m_nla_lemma_vector.reset(); m_nla->check_bounded_divisions(); for (auto & lemma : m_nla->lemmas()) false_case_of_check_nla(lemma); - return m_nla_lemma_vector.empty(); + return m_nla->lemmas.empty(); } expr_ref var2expr(lpvar v) { @@ -3192,7 +3191,6 @@ public: } lp::explanation m_explanation; - vector m_nla_lemma_vector; vector m_nla_literals; literal_vector m_core; svector m_eqs;