diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index fe9a2023c..e7bea94e8 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3368,9 +3368,9 @@ namespace smt {
         }
         if (r == l_true && gparams::get_value("model_validate") == "true") {
             recfun::util u(m);
+            model_ref mdl;
+            get_model(mdl);            
             if (u.get_rec_funs().empty()) {
-                model_ref mdl;
-                get_model(mdl);
                 if (mdl.get()) {
                     for (theory* t : m_theory_set) {
                         t->validate_model(*mdl);
@@ -3384,7 +3384,7 @@ namespace smt {
                 if (lit.sign() ? m_model->is_true(v) : m_model->is_false(v)) {
                     IF_VERBOSE(10, verbose_stream() 
                                << "invalid assignment " << (lit.sign() ? "true" : "false") 
-                               << " to #" << v->get_id() << " := " << mk_bounded_pp(v, m, 2) << "\n");
+                               << " to #" << v->get_id() << " := " << mk_bounded_pp(v, m, 3) << "\n");
                 }
             }
             for (clause* cls : m_aux_clauses) {
diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp
index 51098bafb..94b30bf83 100644
--- a/src/smt/smt_context_inv.cpp
+++ b/src/smt/smt_context_inv.cpp
@@ -374,15 +374,17 @@ namespace smt {
             case l_undef:
                 break;
             case l_true:
-                if (!m_proto_model->eval(n, res, false)) return true;
-                CTRACE("mbqi_bug", !m.is_true(res), tout << n << " evaluates to " << res << "\n";); 
+                if (!m_proto_model->eval(n, res, false)) 
+                    return true;
+                CTRACE("model", !m.is_true(res), tout << n << " evaluates to " << res << "\n";); 
                 if (m.is_false(res)) {
                     return false;
                 }
                 break;
             case l_false:
-                if (!m_proto_model->eval(n, res, false)) return true;
-                CTRACE("mbqi_bug", !m.is_false(res), tout << n << " evaluates to " << res << "\n";); 
+                if (!m_proto_model->eval(n, res, false)) 
+                    return true;
+                CTRACE("model", !m.is_false(res), tout << n << " evaluates to " << res << "\n";); 
                 if (m.is_true(res)) {
                     return false;
                 }
diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
index 80efcc048..b28a0ea5f 100644
--- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp
+++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
@@ -98,13 +98,14 @@ protected:
             return;
         SASSERT(m_solver.get_scope_level() == 0);
         TRACE("ctx_solver_simplify_tactic",
-              for (unsigned i = 0; i < fmls.size(); ++i) {
-                  tout << mk_pp(fmls[i], m) << "\n";
+              for (expr* f : fmls) {
+                  tout << mk_pp(f, m) << "\n";
               }
               tout << "=>\n";
-              tout << mk_pp(fml, m) << "\n";);
+              tout << fml << "\n";);
         DEBUG_CODE(
         {
+            // enable_trace("after_search");
             m_solver.push();
             expr_ref fml1(m);
             fml1 = mk_and(m, fmls.size(), fmls.c_ptr());
@@ -114,9 +115,14 @@ protected:
             lbool is_sat = m_solver.check();
             TRACE("ctx_solver_simplify_tactic", tout << "is non-equivalence sat?: " << is_sat << "\n";);
             if (is_sat == l_true) {
+                model_ref mdl;
+                m_solver.get_model(mdl);
                 TRACE("ctx_solver_simplify_tactic", 
                       tout << "result is not equivalent to input\n";
-                      tout << mk_pp(fml1, m) << "\n";);
+                      tout << mk_pp(fml1, m) << "\n";
+                      tout << "evaluates to: " << (*mdl)(fml1) << "\n";
+                      m_solver.display(tout) << "\n";
+                      );
                 UNREACHABLE();
             }
             m_solver.pop(1);
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 2cef1f7b3..40d648429 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1659,6 +1659,7 @@ public:
     }
 
     final_check_status final_check_eh() {
+        reset_variable_values();
         IF_VERBOSE(12, verbose_stream() << "final-check " << m_solver->get_status() << "\n");
         m_use_nra_model = false;
         lbool is_sat = l_true;