fix #5663

Z3Prover · Nov 12, 2021 · b6f7dea · b6f7dea
1 parent 3c16edc
commit b6f7dea
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git 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
@@ -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: {