From 0b30ddb769ac2e83189d342cc8a403d9f05ebf9d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Jul 2018 02:09:47 -0700 Subject: [PATCH] fix #1733 Signed-off-by: Nikolaj Bjorner --- 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 b4415264b..b105def2c 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2763,12 +2763,12 @@ public: } case lp::lp_status::FEASIBLE: { inf_rational val(term_max.x, term_max.y); - // todo , TODO , not sure what happens here + blocker = mk_gt(v); return inf_eps(rational::zero(), val); } default: SASSERT(st == lp::lp_status::UNBOUNDED); - TRACE("arith", tout << "Unbounded v" << v << "\n";); + TRACE("arith", tout << "Unbounded v" << v << "\n";); has_shared = false; blocker = m.mk_false(); return inf_eps(rational::one(), inf_rational());