From 6d0b89a989827599dfa986bc51dafeae77e7fed7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 22 Nov 2020 15:37:55 -0800
Subject: [PATCH] fix #4810

---
 src/smt/theory_lra.cpp | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 3f99108c4..1f74dd592 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1552,11 +1552,9 @@ public:
         IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n");
         lbool is_sat = l_true;
         SASSERT(lp().ax_is_correct());
-        if (lp().get_status() != lp::lp_status::OPTIMAL) { // || lp().has_changed_columns()) {
+        if (lp().get_status() != lp::lp_status::OPTIMAL || lp().has_changed_columns()) {
             is_sat = make_feasible();
         }
-        else
-            SASSERT(!lp().has_changed_columns());
         final_check_status st = FC_DONE;
 
         switch (is_sat) {
@@ -2088,6 +2086,7 @@ public:
     }
 
     void propagate() {
+        m_model_is_initialized = false;
         flush_bound_axioms();
         if (!can_propagate()) {
             return;