diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 8b542097f..0d6edd3ab 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1154,6 +1154,7 @@ namespace sat {
                 if (mdl[v] != l_true) l.neg();
                 push();
                 assign_core(l, justification(scope_lvl()));
+                propagate(false);
             }
             mk_model();
             break;