fix #4948

Z3Prover · Jan 12, 2021 · fc3a642 · fc3a642
1 parent 0aac7e5
commit fc3a642
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 5 deletions.
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
@@ -252,11 +252,10 @@ namespace opt {
 
         auto decrement = [&]() {
             SASSERT(has_shared);
-            if (l_true != decrement_value(i, val)) {
-                if (l_true != m_context.check(0, nullptr))  
-                    throw default_exception("maximization suspended");
-                m_context.get_model(m_last_model);
-            }
+            decrement_value(i, val);
+            if (l_true != m_context.check(0, nullptr))  
+                throw default_exception("maximization suspended");
+            m_context.get_model(m_last_model);            
         };
 
         if (!val.is_finite()) {

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
@@ -3459,7 +3459,11 @@ class theory_lra::imp {
             st = lp::lp_status::UNBOUNDED;
         }
         else {
+            if (lp().get_status() != lp::lp_status::OPTIMAL || lp().has_changed_columns()) 
+                make_feasible();
+
             vi = get_lpvar(v);
+
             st = lp().maximize_term(vi, term_max);
             if (has_int() && lp().has_inf_int()) {
                 st = lp::lp_status::FEASIBLE;
@@ -3483,6 +3487,7 @@ class theory_lra::imp {
             return inf_eps(rational::zero(), val);
         }
         default:
+            std::cout << st << "\n";
             SASSERT(st == lp::lp_status::UNBOUNDED);
             TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n"););
             has_shared = false;