fix #6265

Z3Prover · Aug 12, 2022 · b6d71fc · b6d71fc
1 parent 03385bf
commit b6d71fc
Showing 1 changed file with 8 additions and 13 deletions.
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -3507,16 +3507,15 @@ class theory_lra::imp {
         case lp::lp_status::OPTIMAL: {
             init_variable_values();
             TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n"););
-            inf_rational val = get_value(v);
-            // inf_rational val(term_max.x, term_max.y);
+            auto val = value(v);
             blocker = mk_gt(v);
-            return inf_eps(rational::zero(), val);
+            return val;
         }
         case lp::lp_status::FEASIBLE: {
-            inf_rational val = get_value(v);
+            auto val = value(v);
             TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n"););
             blocker = mk_gt(v);
-            return inf_eps(rational::zero(), val);
+            return val;
         }
         default:
             SASSERT(st == lp::lp_status::UNBOUNDED);
@@ -3533,23 +3532,19 @@ class theory_lra::imp {
         rational r = val.x;
         expr_ref e(m);
         if (a.is_int(obj->get_sort())) {
-            if (r.is_int()) {
+            if (r.is_int()) 
                 r += rational::one();
-            }
-            else {
+            else 
                 r = ceil(r);
-            }
             e = a.mk_numeral(r, obj->get_sort());
             e = a.mk_ge(obj, e);
         }
         else {
             e = a.mk_numeral(r, obj->get_sort());
-            if (val.y.is_neg()) {
+            if (val.y.is_neg()) 
                 e = a.mk_ge(obj, e);
-            }
-            else {
+            else 
                 e = a.mk_gt(obj, e);
-            }
         }
         TRACE("opt", tout << "v" << v << " " << val << " " << r << " " << e << "\n";);
         return e;