From 8258e2a8fdfcef4528906c8eda998614d08d22dc Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 14 Jun 2019 17:47:03 -0700 Subject: [PATCH] generate lemmas from nla_intervals Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index d2aeacd33..f143bd3c8 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2327,7 +2327,7 @@ public: struct local_bound_propagator: public lp::lp_bound_propagator { imp & m_imp; - local_bound_propagator(imp& i) : lp_bound_propagator(*i.m_solver, i.get_nla_solver()), m_imp(i) {} + local_bound_propagator(imp& i) : lp_bound_propagator(*i.m_solver), m_imp(i) {} bool bound_is_interesting(unsigned j, lp::lconstraint_kind kind, const rational & v) override { return m_imp.bound_is_interesting(j, kind, v); @@ -2375,7 +2375,7 @@ public: m_params.reset(); m_explanation.clear(); local_bound_propagator bp(*this); - bp.explain_implied_bound(be); + lp().explain_implied_bound(be, bp); } CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";); updt_unassigned_bounds(v, -1);