diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index b2342314e..c240286fa 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -205,7 +205,7 @@ namespace polysat {
     }
 
     bool viable::intersect(pvar v, entry* ne) {
-        SASSERT(!s.is_assigned(v));
+        // SASSERT(!s.is_assigned(v));  // TODO: do we get unsoundness if this condition is violated? (see comment on cyclic dependencies in solver::pop_levels)
         entry* e = m_units[v];
         if (e && e->interval.is_full()) {
             m_alloc.push_back(ne);