diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 2a3715f2d..d28d2a7a3 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -208,6 +208,8 @@ namespace polysat {
 #endif
         push_qhead();
         while (can_propagate()) {
+            if (is_conflict())
+                return;
             auto const& item = m_search[m_qhead++];
             if (item.is_assignment())
                 propagate(item.var());