diff --git a/src/math/polysat/op_constraint.cpp b/src/math/polysat/op_constraint.cpp
index 7f5ebd86c..b8b5384fc 100644
--- a/src/math/polysat/op_constraint.cpp
+++ b/src/math/polysat/op_constraint.cpp
@@ -662,8 +662,6 @@ namespace polysat {
         rational prodv = (pv * rv).val();
         if (prodv != rational::power_of_two(parity_pv))
             verbose_stream() << prodv << " " << rational::power_of_two(parity_pv) << " " << parity_pv << " " << pv << " " << rv << "\n";
-        SASSERT(prodv != rational::power_of_two(parity_pv)); // Why did it evaluate to false in this case?
-        VERIFY(prodv != rational::power_of_two(parity_pv)); // Why did it evaluate to false in this case?
         unsigned lower = 0, upper = m.power_of_2();
         // binary search for the parity (otw. we would have justifications like "parity_at_most(k) && parity_at_least(k)" for at most "k" widths
         while (lower + 1 < upper) {
@@ -688,6 +686,7 @@ namespace polysat {
             if (rv.val() > max_rv)
                 return s.mk_clause(~invc, s.parity_at_least(p(), middle), s.ule(r(), max_rv), false);
         }
+         // Why did it evaluate to false in this case?
         UNREACHABLE();
         return {};
     }