diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index cdbbb365b..d7df0a85b 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -1672,6 +1672,17 @@ namespace sat {
                     change = true;
                     last_changed = lit;
                 }
+                {
+                    // if l was derived from lit and ~lit -> l, then l is a necessary assignment
+                    scoped_level _sl(*this, dl_lvl);
+                    literal_vector const& lits = m_binary[(~l).index()];
+                    for (literal l : lits) {
+                        if (inconsistent()) break;
+                        if (is_true(l) && !is_fixed_at(l, cl_fixed_truth)) {
+                            assign(l);
+                        }
+                    }
+                }
                 SASSERT(inconsistent() || !is_unsat());
             }
             if (c_fixed_truth - 2 * m_lookahead.size() < base) {
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index fce4fd636..14bfbb582 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -501,7 +501,6 @@ namespace sat {
         unsigned do_double(literal l, unsigned& base);
         unsigned double_look(literal l, unsigned& base);
         void set_conflict() { TRACE("sat", tout << "conflict\n";); m_inconsistent = true; }
-        //void set_conflict() { TRACE("sat", tout << "conflict\n";); printf("CONFLICT\n"); m_inconsistent = true; }
         bool inconsistent() { return m_inconsistent; }
 
         unsigned scope_lvl() const { return m_trail_lim.size(); }