From fc3a642876cddfca38840d5e1b41cfb657e98a28 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 11 Jan 2021 19:26:16 -0800
Subject: [PATCH] fix #4948

---
 src/opt/opt_solver.cpp | 9 ++++-----
 src/smt/theory_lra.cpp | 5 +++++
 2 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 5686e1afd..abe256eaa 100644
--- 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
index 9abe7e53e..b7e47532f 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3459,7 +3459,11 @@ public:
             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 @@ public:
             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;