From b6f7deacf4dbdefc3672524b80ae1af7fa1e0507 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 12 Nov 2021 11:36:42 -0800
Subject: [PATCH] fix #5663

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

diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 0bc7ba98654..21489be58e1 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -305,11 +305,9 @@ namespace opt {
         expr_ref fml(m), bound(m.mk_true(), m), tmp(m);
         expr* vars[1];
         {
-            for (unsigned i = 0; i < m_upper.size(); ++i) {
+            for (unsigned i = 0; i < m_upper.size(); ++i) 
                 ors.push_back(m_s->mk_ge(i, m_upper[i]));
-            }
-            
-            
+                        
             fml = mk_or(ors);
             tmp = m.mk_fresh_const("b", m.mk_bool_sort());
             fml = m.mk_implies(tmp, fml);
@@ -328,8 +326,7 @@ namespace opt {
                     m_s->get_model(m_model);       
                     m_s->get_labels(m_labels);            
                     for (unsigned i = 0; i < ors.size(); ++i) {
-                        expr_ref tmp(m);
-                        if (m_model->is_true(ors[i].get())) {
+                        if (m_model->is_true(ors.get(i))) {       
                             m_lower[i] = m_upper[i];
                             ors[i]  = m.mk_false();
                             disj[i] = m.mk_false();
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 88fdb3d8849..4931c990084 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3477,7 +3477,10 @@ class theory_lra::imp {
                 st = lp::lp_status::FEASIBLE;
                 lp().restore_x();
             }
-                
+            if (m_nla && st == lp::lp_status::OPTIMAL) {
+                st = lp::lp_status::FEASIBLE;
+                lp().restore_x();
+            }                
         }
         switch (st) {
         case lp::lp_status::OPTIMAL: {