From 182fea2d7ba77c8ceec8b974d5e3729ef3bd84fe Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 5 May 2014 10:21:16 -0700
Subject: [PATCH] fix bcd2

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/maxsmt.cpp          | 4 ++--
 src/opt/opt_context.cpp     | 7 ++-----
 src/opt/weighted_maxsat.cpp | 1 +
 3 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index cc1b1ba42..1f43bbe36 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -91,7 +91,7 @@ namespace opt {
         rational r = m_lower;
         if (m_msolver) {
             rational q = m_msolver->get_lower();
-            if (r < q) r = q;
+            if (q > r) r = q;
         }
         return r;
     }
@@ -100,7 +100,7 @@ namespace opt {
         rational r = m_upper;
         if (m_msolver) {
             rational q = m_msolver->get_upper();
-            if (r > q) r = q;
+            if (q < r) r = q;
         }
         return r;
     }
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 4f2a5eba2..7b9ca0a8d 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -612,7 +612,6 @@ namespace opt {
         return mk_objective_fn(index, O_MAXSMT, num_fmls, fmls);
     }
 
-
     void context::from_fmls(expr_ref_vector const& fmls) {
         TRACE("opt",
               for (unsigned i = 0; i < fmls.size(); ++i) {
@@ -625,7 +624,7 @@ namespace opt {
             app_ref tr(m);
             expr_ref_vector terms(m);
             vector<rational> weights;
-            rational offset;
+            rational offset(0);
             unsigned index;
             symbol id;
             bool neg;
@@ -737,7 +736,7 @@ namespace opt {
                     }
                 }
                 if (ok) {
-                    m_maxsmts.find(obj.m_id)->update_lower(r, override);
+                    m_maxsmts.find(obj.m_id)->update_upper(r, override);
                 }
                 break;
             }
@@ -749,7 +748,6 @@ namespace opt {
         
     }
 
-
     void context::display_assignment(std::ostream& out) {
         for (unsigned i = 0; i < m_objectives.size(); ++i) {
             objective const& obj = m_objectives[i];
@@ -763,7 +761,6 @@ namespace opt {
         }
     }
 
-
     void context::display_objective(std::ostream& out, objective const& obj) const {
         switch(obj.m_type) {
         case O_MAXSMT: {
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index 593e87e7f..7a19e00af 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -300,6 +300,7 @@ namespace opt {
                         unsigned s = *subC.begin();
                         wcore& c_s = m_cores[s];
                         c_s.m_lower = refine(c_s.m_R, c_s.m_mid);
+                        c_s.m_mid = div(c_s.m_lower + c_s.m_upper, rational(2));
                     }
                     else {
                         wcore c_s;