From 50f18a77af88b20083bf2116afd71cf6c850c626 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 15 Dec 2013 02:40:52 +0200
Subject: [PATCH] disable 'optimization' that led to wrong model'

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/arith_decl_plugin.cpp | 1 +
 src/opt/fu_malik.cpp          | 4 +++-
 src/opt/opt_context.cpp       | 7 +++++--
 src/opt/opt_solver.cpp        | 2 ++
 4 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp
index 9d1f4343f..5245b9685 100644
--- a/src/ast/arith_decl_plugin.cpp
+++ b/src/ast/arith_decl_plugin.cpp
@@ -417,6 +417,7 @@ inline decl_kind arith_decl_plugin::fix_kind(decl_kind k, unsigned arity) {
 
 app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
     if (is_int && !val.is_int()) {
+        SASSERT(false);
         m_manager->raise_exception("invalid rational value passed as an integer");
     }
     if (val.is_unsigned()) {
diff --git a/src/opt/fu_malik.cpp b/src/opt/fu_malik.cpp
index 4114ac080..db6a017b2 100644
--- a/src/opt/fu_malik.cpp
+++ b/src/opt/fu_malik.cpp
@@ -25,6 +25,7 @@ Notes:
 #include "tactic.h"
 #include "smt_context.h"
 #include "ast_pp.h"
+#include "model_smt2_pp.h"
 
 /**
    \brief Fu & Malik procedure for MaxSAT. This procedure is based on 
@@ -323,7 +324,8 @@ namespace opt {
                     VERIFY(m_model->eval(m_orig_soft[i].get(), val));
                     m_assignment.push_back(m.is_true(val));                        
                 }
-                TRACE("opt", tout << "maxsat cost: " << m_upper << "\n";);
+                TRACE("opt", tout << "maxsat cost: " << m_upper << "\n";
+                      model_smt2_pp(tout, m, *m_model, 0););
             }
             // We are done and soft_constraints has 
             // been updated with the max-sat assignment.            
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 749fa071d..48274c502 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -122,7 +122,7 @@ namespace opt {
     lbool context::execute_min_max(unsigned index, bool committed) {
         lbool result = m_optsmt.lex(index);
         if (committed) m_optsmt.commit_assignment(index);
-        if (committed && result == l_true) m_optsmt.get_model(m_model);
+        if (result == l_true) m_optsmt.get_model(m_model);
         return result;
     }
 
@@ -130,7 +130,7 @@ namespace opt {
         maxsmt& ms = *m_maxsmts.find(id);
         lbool result = ms(get_solver());
         if (committed) ms.commit_assignment();
-        if (committed && result == l_true) ms.get_model(m_model);
+        if (result == l_true) ms.get_model(m_model);
         return result;
     }
 
@@ -736,6 +736,9 @@ namespace opt {
                 maxsmt& ms = *m_maxsmts.find(obj.m_id);
                 for (unsigned i = 0; i < obj.m_terms.size(); ++i) {
                     VERIFY(m_model->eval(obj.m_terms[i], val));
+                    CTRACE("opt",ms.get_assignment(i) != (m.mk_true() == val), 
+                           tout << mk_pp(obj.m_terms[i], m) << " evaluates to " << val << "\n";
+                           model_smt2_pp(tout, m, *m_model, 0););
                     SASSERT(ms.get_assignment(i) == (m.mk_true() == val));
                 }
                 break;
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index 8ed4c863d..4dbe08697 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -26,6 +26,7 @@ Notes:
 #include "ast_pp.h"
 #include "ast_smt_pp.h"
 #include "pp_params.hpp"
+#include "model_smt2_pp.h"
 
 namespace opt {
 
@@ -130,6 +131,7 @@ namespace opt {
         smt::theory_var v = m_objective_vars[i];
         m_objective_values[i] = get_optimizer().maximize(v);
         m_context.get_context().update_model();        
+        TRACE("opt", { model_ref mdl; get_model(mdl); model_smt2_pp(tout << "update model: ", m, *mdl, 0); });
     }
     
     void opt_solver::get_unsat_core(ptr_vector<expr> & r) {