diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index 9a0740cb5..c9552d5d2 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -1626,6 +1626,7 @@ namespace sat {
                 pop_lookahead1(lit, num_units); 
                 if (unsat) {
                     TRACE("sat", tout << "backtracking and settting " << ~lit << "\n";);
+                    lookahead_backtrack();
                     assign(~lit);
                     propagate();
                     change = true;