diff --git a/src/math/polysat/mul_ovfl_constraint.cpp b/src/math/polysat/mul_ovfl_constraint.cpp
index 441b68876..33b2b1113 100644
--- a/src/math/polysat/mul_ovfl_constraint.cpp
+++ b/src/math/polysat/mul_ovfl_constraint.cpp
@@ -140,7 +140,6 @@ namespace polysat {
         clause_ref just = cb.build();
         SASSERT(just);
         s.add_clause(*just);
-        s.propagate();
         SASSERT(s.m_bvars.is_true(conseq.blit()));
         return true;
     }