diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 4bb7ba180..b15a32e32 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -340,6 +340,13 @@ namespace sat {
     }
 
     bool lookahead::is_unsat() const {
+        for (unsigned idx = 0; idx < m_binary.size(); ++idx) {
+            literal l = to_literal(idx);
+            for (literal lit : m_binary[idx]) {
+                if (is_true(l) && is_false(lit))
+                    return true;
+            }
+        }
         // check if there is a clause whose literals are false.
         // every clause is terminated by a null-literal.
         for (nary* n : m_nary_clauses) {
@@ -440,8 +447,21 @@ namespace sat {
 
     bool lookahead::missed_conflict() const {
         if (inconsistent()) return false;
+        for (literal l1 : m_trail) {
+            for (literal l2 : m_binary[l1.index()]) {
+                if (is_false(l2))
+                    return true;
+            }
+            unsigned sz = m_ternary_count[(~l1).index()];
+            for (binary b : m_ternary[(~l1).index()]) {
+                if (sz-- == 0) break;
+                if ((is_false(b.m_u) && is_false(b.m_v)))
+                    return true;
+            }
+        }
         for (nary * n : m_nary_clauses) {
-            if (n->size() == 0) return true;
+            if (n->size() == 0)
+                return true;
         }
         return false;
     }
@@ -1464,7 +1484,7 @@ namespace sat {
         sz = m_nary_count[l.index()];
         for (nary* n : m_nary[l.index()]) {
             if (sz-- == 0) break;
-            if (m_stamp[l.var()] > m_stamp[n->get_head().var()]) {
+            if (get_level(l) > get_level(n->get_head())) {
                 n->set_head(l);
             }
         }
@@ -1660,6 +1680,7 @@ namespace sat {
                     num_units += do_double(lit, dl_lvl);
                     if (dl_lvl > level) {
                         base = dl_lvl;
+                        SASSERT(get_level(m_trail.back()) == base + m_lookahead[i].m_offset);
                     }
                     unsat = inconsistent();
                     pop_lookahead1(lit, num_units);
@@ -1785,11 +1806,12 @@ namespace sat {
         base += m_lookahead.size();
         unsigned dl_truth = base + m_lookahead.size() * m_config.m_dl_max_iterations;
         scoped_level _sl(*this, dl_truth);
+        SASSERT(get_level(m_trail.back()) == dl_truth);
+        SASSERT(is_fixed(l));
         IF_VERBOSE(2, verbose_stream() << "double: " << l << " depth: " << m_trail_lim.size() << "\n";);
         lookahead_backtrack();
         assign(l);
         propagate();
-        //SASSERT(!inconsistent());
         unsigned old_sz = m_trail.size();
         bool change = true;
         literal last_changed = null_literal;
@@ -1830,6 +1852,8 @@ namespace sat {
             base += 2 * m_lookahead.size();
             SASSERT(dl_truth >= base);
         }
+        lookahead_backtrack();
+        SASSERT(get_level(m_trail.back()) == dl_truth);
         SASSERT(m_level == dl_truth);
         base = dl_truth;
         return m_trail.size() - old_sz;
@@ -1848,6 +1872,7 @@ namespace sat {
         if (is_undef(l)) {
             TRACE("sat", tout << "assign: " << l << " @ " << m_level << " " << m_trail_lim.size() << " " << m_search_mode << "\n";);
             set_true(l);
+            SASSERT(m_trail.empty() || get_level(m_trail.back()) >= get_level(l));
             m_trail.push_back(l);
             if (m_search_mode == lookahead_mode::searching) {
                 m_stats.m_propagations++;
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index 64a4ef63e..e84213cfe 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -90,7 +90,7 @@ namespace sat {
                 m_min_cutoff = 30;
                 m_preselect = false;
                 m_level_cand = 600;
-                m_delta_rho = (double)0.85;
+                m_delta_rho = (double)0.7;
                 m_dl_max_iterations = 2;
                 m_tc1_limit = 10000000;
                 m_reward_type = ternary_reward;
@@ -246,8 +246,8 @@ namespace sat {
         inline bool is_true(literal l) const { return is_true_at(l, m_level); }
         inline void set_true(literal l) { m_stamp[l.var()] = m_level + l.sign(); }
         inline void set_undef(literal l) { m_stamp[l.var()] = 0; }
+        inline unsigned get_level(literal l) const { return m_stamp[l.var()] & UINT_MAX - 1; }
         void set_level(literal d, literal s) { m_stamp[d.var()] = (m_stamp[s.var()] & ~0x1) + d.sign(); }
-        unsigned get_level(literal d) const { return m_stamp[d.var()]; }
         lbool value(literal l) const { return is_undef(l) ? l_undef : is_true(l) ? l_true : l_false; }
         
         // set the level within a scope of the search.