From 97b2fc9ee7fef4e2e161f764a235bd602d6d8b11 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 8 Dec 2013 18:34:28 -0800
Subject: [PATCH] fix bugs exposed by testSolver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp              | 20 ++++++++++++++++----
 src/opt/optsmt.cpp                   | 12 ++++++++++++
 src/tactic/arith/lia2card_tactic.cpp |  6 ++++++
 3 files changed, 34 insertions(+), 4 deletions(-)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 1bb34f6dd..9e6a9fae6 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -419,7 +419,7 @@ namespace opt {
         for (unsigned i = 0; i < m_objectives.size(); ++i) {
             objective const& obj = m_objectives[i];
             display_objective(out, obj);
-            out << get_upper(i) << "\n";
+            out << "|-> " << get_upper(i) << "\n";
         }
     }
 
@@ -427,7 +427,7 @@ namespace opt {
         for (unsigned i = 0; i < m_objectives.size(); ++i) {            
             objective const& obj = m_objectives[i];
             display_objective(out, obj);
-            out << " [" << get_lower(i) << ":" << get_upper(i) << "]\n";
+            out << " |-> [" << get_lower(i) << ":" << get_upper(i) << "]\n";
         }
     }
 
@@ -496,13 +496,25 @@ namespace opt {
         expr_ref_vector args(m);
         arith_util a(m);
         if (!inf.is_zero()) {
-            args.push_back(a.mk_mul(a.mk_numeral(inf, inf.is_int()), m.mk_const(symbol("oo"), a.mk_int())));
+            expr* oo = m.mk_const(symbol("oo"), a.mk_int());
+            if (inf.is_one()) {
+                args.push_back(oo);
+            }
+            else {
+                args.push_back(a.mk_mul(a.mk_numeral(inf, inf.is_int()), oo));
+            }
         }
         if (!r.is_zero()) {
             args.push_back(a.mk_numeral(r, r.is_int()));
         }
         if (!eps.is_zero()) {
-            args.push_back(a.mk_mul(a.mk_numeral(eps, eps.is_int()), m.mk_const(symbol("epsilon"), a.mk_int())));
+            expr* ep = m.mk_const(symbol("epsilon"), a.mk_int());
+            if (eps.is_one()) {
+                args.push_back(ep);
+            }
+            else {
+                args.push_back(a.mk_mul(a.mk_numeral(eps, eps.is_int()), ep));
+            }
         }
         switch(args.size()) {
         case 0: return expr_ref(a.mk_numeral(rational(0), true), m);
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index e8df01b5a..2f4a35459 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -79,6 +79,12 @@ namespace opt {
         if (m_cancel || is_sat == l_undef) {
             return l_undef;
         }
+
+        // set the solution tight.
+        for (unsigned i = 0; i < m_lower.size(); ++i) {
+            m_upper[i] = m_lower[i];
+        }
+        
         return l_true;        
     }
 
@@ -102,6 +108,12 @@ namespace opt {
         if (m_cancel || is_sat == l_undef) {
             return l_undef;
         }
+
+        // set the solution tight.
+        for (unsigned i = 0; i < m_lower.size(); ++i) {
+            m_upper[i] = m_lower[i];
+        }
+
         return l_true;        
     }
 
diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp
index 347d4749f..f5ae23b07 100644
--- a/src/tactic/arith/lia2card_tactic.cpp
+++ b/src/tactic/arith/lia2card_tactic.cpp
@@ -163,6 +163,9 @@ public:
     }
 
     expr* mk_le(unsigned sz, rational const* weights, expr* const* args, rational const& w) {
+        if (sz == 0) {
+            return w.is_neg()?m.mk_false():m.mk_true();
+        }
         if (sz == 1 && weights[0].is_one() && w >= rational::one()) {
             return m.mk_true();
         }
@@ -173,6 +176,9 @@ public:
     }
     
     expr* mk_ge(unsigned sz, rational const* weights, expr* const* args, rational const& w) {
+        if (sz == 0) {
+            return w.is_pos()?m.mk_false():m.mk_true();
+        }
         if (sz == 1 && weights[0].is_one() && w.is_one()) {
             return args[0];
         }