diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index faa9b639e..ab2352253 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -1556,7 +1556,7 @@ namespace sat {
             m_learned.push_back(c);
         }
         else {
-            SASSERT(s().at_base_lvl());
+            SASSERT(!m_solver || s().at_base_lvl());
             m_constraints.push_back(c);
         }
         literal lit = c->lit();
diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h
index 3e02d49dc..09903f889 100644
--- a/src/sat/ba_solver.h
+++ b/src/sat/ba_solver.h
@@ -362,8 +362,8 @@ namespace sat {
         // access solver
         inline lbool value(bool_var v) const { return value(literal(v, false)); }
         inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); }
-        inline unsigned lvl(literal lit) const { return m_solver->lvl(lit); }
-        inline unsigned lvl(bool_var v) const { return m_solver->lvl(v); }
+        inline unsigned lvl(literal lit) const { return m_lookahead ? 0 : m_solver->lvl(lit); }
+        inline unsigned lvl(bool_var v) const { return m_lookahead ? 0 : m_solver->lvl(v); }
         inline bool inconsistent() const { return m_lookahead ? m_lookahead->inconsistent() : m_solver->inconsistent(); }
         inline watch_list& get_wlist(literal l) { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); }
         inline watch_list const& get_wlist(literal l) const { return m_lookahead ? m_lookahead->get_wlist(l) : m_solver->get_wlist(l); }
diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index f607d53ad..5c039f664 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -408,6 +408,7 @@ namespace sat {
     }
 
     bool lookahead::missed_propagation() const {
+        if (inconsistent()) return false;
         for (literal l1 : m_trail) {
             SASSERT(is_true(l1));
             for (literal l2 : m_binary[l1.index()]) {
@@ -1614,7 +1615,7 @@ namespace sat {
         }
         SASSERT(m_qhead == m_trail.size() || (inconsistent() && m_qhead < m_trail.size()));
         //SASSERT(!missed_conflict());
-        //SASSERT(inconsistent() || !missed_propagation());
+        VERIFY(!missed_propagation());
         TRACE("sat_verbose", display(tout << scope_lvl() << " " << (inconsistent()?"unsat":"sat") << "\n"););
     }
 
@@ -1656,6 +1657,7 @@ namespace sat {
                     unsat = inconsistent();
                     pop_lookahead1(lit, num_units);
                 }
+                // VERIFY(!missed_propagation());
                 if (unsat) {
                     TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";);
                     lookahead_backtrack();