diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 081c5767d..4d31cb8b3 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -294,8 +294,8 @@ namespace polysat {
             return false;
         }
 
-        if (conflict_var() == v && s.m_viable.resolve(v, *this))
-            return true;
+        // forbidden interval projection is performed at top level
+        SASSERT(v != conflict_var());
         
         m_vars.remove(v);
 
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 1d09a600c..0405bc801 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -473,7 +473,7 @@ namespace polysat {
 
         if (m_conflict.conflict_var() != null_var) {
             // This case corresponds to a propagation of conflict_var, except it's not explicitly on the stack.
-            resolve_value(m_conflict.conflict_var());
+            VERIFY(m_viable.resolve(m_conflict.conflict_var(), m_conflict));
         }
 
         search_iterator search_it(m_search);