diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index a5c9005df..8a75e8dfc 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -123,6 +123,7 @@ namespace sat {
     // -----------------------
 
     bool_var solver::mk_var(bool ext, bool dvar) {
+        m_model_is_current = false;
         m_stats.m_mk_var++;
         bool_var v = m_level.size();
         m_watches.push_back(watch_list());
@@ -148,6 +149,7 @@ namespace sat {
     }
 
     void solver::mk_clause(unsigned num_lits, literal * lits) {
+        m_model_is_current = false;
         DEBUG_CODE({
             for (unsigned i = 0; i < num_lits; i++)
                 SASSERT(m_eliminated[lits[i].var()] == false);
@@ -3118,7 +3120,11 @@ namespace sat {
 
     lbool solver::get_consequences(literal_vector const& asms, bool_var_vector const& vars, vector<literal_vector>& conseq) {
         literal_vector lits;
-        lbool is_sat = check(asms.size(), asms.c_ptr());
+        lbool is_sat = l_true;
+
+        if (!m_model_is_current) {
+            is_sat = check(asms.size(), asms.c_ptr());
+        }
         if (is_sat != l_true) {
             return is_sat;
         }
@@ -3212,6 +3218,12 @@ namespace sat {
                        << " unfixed: " << lits.size() - conseq.size() - vars.size()
                        << ")\n";);
 
+            if (!vars.empty() && 
+                m_config.m_restart_max != 0 &&
+                m_config.m_restart_max <= num_iterations) {
+                return l_undef;
+            }
+
         }
         return l_true;
     }
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index e3a220cd2..6d3a5b552 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -257,7 +257,7 @@ public:
         r = internalize_vars(vars, bvars);
 
         r = m_solver.get_consequences(m_asms, bvars, lconseq);
-        if (r != l_true) return r;
+        if (r == l_false) return r;
 
         // build map from bound variables to 
         // the consequences that cover them.
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 1885fc9c4..507cb6d43 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -1752,7 +1752,7 @@ namespace smt {
         //    verbose_stream() << "(pb.conflict min size: " << l_size << ")\n";
         //    s_min_l_size = l_size;        
         //}
-        //IF_VERBOSE(1, verbose_stream() << "(pb.conflict " << m_ineq_literals.size() << " " << m_lemma.size() << "\n";);
+        IF_VERBOSE(1, verbose_stream() << "(pb.conflict " << m_ineq_literals.size() << " " << m_lemma.size() << ")\n";);
         switch(is_true) {
         case l_true:
             UNREACHABLE();