From b3e1e302f701963bf998a7694391b70e59d20c57 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 18 Mar 2020 13:22:17 -0700
Subject: [PATCH] fix #3320

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/maxlex.cpp     |  2 +-
 src/opt/opt_solver.cpp | 12 ++++++++----
 2 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp
index b29c069ef..5ef028d44 100644
--- a/src/opt/maxlex.cpp
+++ b/src/opt/maxlex.cpp
@@ -82,7 +82,7 @@ namespace opt {
                 if (first_undef && soft.value != l_undef) {
                     continue;
                 }
-                if (first_undef) {
+                else if (first_undef) {
                     SASSERT(soft.value == l_undef);
                     soft.set_value(l_true);
                     assert_value(soft);            
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 0458c2b38..de88b9257 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -292,7 +292,7 @@ namespace opt {
         TRACE("opt", tout << is_sat << "\n";);
         if (is_sat != l_true) {
             // cop-out approximation
-            if (arith_util(m).is_real(m_objective_terms[i].get())) {
+            if (arith_util(m).is_real(m_objective_terms.get(i))) {
                 val -= inf_eps(inf_rational(rational(0), true));
             }
             else {
@@ -382,9 +382,13 @@ namespace opt {
         return get_optimizer().value(v);
     }
     
-    expr_ref opt_solver::mk_ge(unsigned var, inf_eps const& val) {
-        if (!val.is_finite()) {
-            return expr_ref(val.is_pos() ? m.mk_false() : m.mk_true(), m);
+    expr_ref opt_solver::mk_ge(unsigned var, inf_eps const& _val) {
+        if (!_val.is_finite()) {
+            return expr_ref(_val.is_pos() ? m.mk_false() : m.mk_true(), m);
+        }
+        inf_eps val = _val;
+        if (val.get_infinitesimal().is_neg()) {
+            val = inf_eps(val.get_rational());
         }
         smt::theory_opt& opt = get_optimizer();
         smt::theory_var v = m_objective_vars[var];