diff --git a/src/model/model.h b/src/model/model.h
index 9399be285..cfc44a8fc 100644
--- a/src/model/model.h
+++ b/src/model/model.h
@@ -94,5 +94,7 @@ public:
     };
 };
 
+std::ostream& operator<<(std::ostream& out, model_core const& m);
+
 
 #endif /* MODEL_H_ */
diff --git a/src/model/model_smt2_pp.h b/src/model/model_smt2_pp.h
index b38bd631d..c43e26ca6 100644
--- a/src/model/model_smt2_pp.h
+++ b/src/model/model_smt2_pp.h
@@ -25,6 +25,5 @@ Revision History:
 
 void model_smt2_pp(std::ostream & out, ast_printer_context & ctx, model_core const & m, unsigned indent);
 void model_smt2_pp(std::ostream & out, ast_manager & m, model_core const & md, unsigned indent);
-std::ostream& operator<<(std::ostream& out, model_core const& m);
 
 #endif
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index a8d6d5ebe..acfee574a 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1347,7 +1347,7 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core,
 
     if (is_sat == l_true || is_sat == l_undef) {
         if (core) { core->reset(); }
-        if (model && *model) {
+        if (model && model->get()) {
             r = find_rule(**model, is_concrete, reach_pred_used, num_reuse_reach);
             TRACE ("spacer", tout << "reachable "
                    << "is_concrete " << is_concrete << " rused: ";
diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index 78dcbfd16..2f44983ff 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -31,7 +31,6 @@ Revision History:
 #include "qe/qe_arrays.h"
 #include "qe/qe_datatypes.h"
 #include "qe/qe_lite.h"
-#include "model/model_pp.h"
 #include "model/model_evaluator.h"
 
 
@@ -617,26 +616,25 @@ public:
             qe::array_project_plugin ap(m);
             ap(mdl, array_vars, fml, vars, m_reduce_all_selects);
             SASSERT (array_vars.empty ());
-            m_rw (fml);
+            m_rw(fml);
             SASSERT (!m.is_false (fml));
 
             TRACE ("qe",
-                   tout << "extended model:\n";
-                   model_pp (tout, mdl);
+                   tout << "extended model:\n" << mdl;
                    tout << "Vars: " << vars << "\n";
                    );            
         }
                         
         // project reals, ints and other variables.
         if (!other_vars.empty ()) {
-            TRACE ("qe", tout << "Other vars: " << other_vars << "\n";
-                   model_pp(tout, mdl););
+            TRACE ("qe", tout << "Other vars: " << other_vars << "\n" << mdl;);
                         
             expr_ref_vector fmls(m);
             flatten_and (fml, fmls);
             
             (*this)(false, other_vars, mdl, fmls);
             fml = mk_and (fmls);
+            m_rw(fml);
                         
             TRACE ("qe",
                    tout << "Projected other vars:\n" << fml << "\n";
@@ -646,14 +644,15 @@ public:
         
         if (!other_vars.empty ()) {
             project_vars (mdl, other_vars, fml);
+            m_rw(fml);
         }
         
         // substitute any remaining other vars
         if (!m_dont_sub && !other_vars.empty ()) {
             subst_vars (eval, other_vars, fml);
-            TRACE ("qe", tout << "After substituting remaining other vars:\n" << fml << "\n";);
             // an extra round of simplification because subst_vars is not simplifying
             m_rw(fml);
+            TRACE ("qe", tout << "After substituting remaining other vars:\n" << fml << "\n";);
             other_vars.reset();
         }