From a549e73b86967989d55e99f2e008aa5348909d0b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 4 Oct 2018 13:43:01 -0700
Subject: [PATCH] na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp    | 4 +---
 src/opt/opt_pareto.cpp     | 2 +-
 src/smt/theory_arith_aux.h | 5 ++++-
 3 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 87da85af5..74d1ca955 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -479,7 +479,6 @@ namespace opt {
         return r;
     }
 
-
     expr_ref context::mk_le(unsigned i, model_ref& mdl) {
         objective const& obj = m_objectives[i];
         return mk_cmp(false, mdl, obj);
@@ -489,8 +488,7 @@ namespace opt {
         objective const& obj = m_objectives[i];
         return mk_cmp(true, mdl, obj);
     }
-    
-    
+        
     expr_ref context::mk_gt(unsigned i, model_ref& mdl) {
         expr_ref result = mk_le(i, mdl);
         result = mk_not(m, result);
diff --git a/src/opt/opt_pareto.cpp b/src/opt/opt_pareto.cpp
index fe92c3ba6..ada5d0d14 100644
--- a/src/opt/opt_pareto.cpp
+++ b/src/opt/opt_pareto.cpp
@@ -71,7 +71,7 @@ namespace opt {
         fmls.push_back(mk_or(gt));
         fml = mk_and(fmls);
         IF_VERBOSE(10, verbose_stream() << "dominates: " << fml << "\n";);
-        TRACE("opt", tout << fml << "\n"; model_smt2_pp(tout, m, *m_model, 0););
+        TRACE("opt", model_smt2_pp(tout << fml << "\n", m, *m_model, 0););
         m_solver->assert_expr(fml);        
     }
 
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 9526637e9..89737fb42 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1103,6 +1103,7 @@ namespace smt {
                 e = m_util.mk_gt(obj, e);
             }
         }
+        TRACE("opt", tout << e << "\n";);
         return e;
     }
 
@@ -1119,6 +1120,8 @@ namespace smt {
         std::ostringstream strm;
         strm << val << " <= " << mk_pp(get_enode(v)->get_owner(), get_manager());
         app* b = m.mk_const(symbol(strm.str().c_str()), m.mk_bool_sort());
+        expr_ref result(b, m);
+        TRACE("opt", tout << result << "\n";);
         if (!ctx.b_internalized(b)) {
             fm.hide(b->get_decl());
             bool_var bv = ctx.mk_bool_var(b);
@@ -1133,7 +1136,7 @@ namespace smt {
             TRACE("arith", tout << mk_pp(b, m) << "\n";
                   display_atom(tout, a, false););            
         }
-        return expr_ref(b, m);
+        return result;
     }