diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp
index a605faa89..22acc2b12 100644
--- a/src/math/polysat/forbidden_intervals.cpp
+++ b/src/math/polysat/forbidden_intervals.cpp
@@ -166,11 +166,11 @@ namespace polysat {
         _backtrack.released = true;
 
         // v > q
-        if (ok1 && !ok2 && match_non_zero(c, a1, b1, e1, c->to_ule().rhs(), fi))
+        if (false && ok1 && !ok2 && match_non_zero(c, a1, b1, e1, c->to_ule().rhs(), fi))
             return true;
 
         // p > v
-        if (!ok1 && ok2 && match_non_max(c, c->to_ule().lhs(), a2, b2, e2, fi))
+        if (false && !ok1 && ok2 && match_non_max(c, c->to_ule().lhs(), a2, b2, e2, fi))
             return true;
 
         if (!ok1 || !ok2 || (a1.is_zero() && a2.is_zero())) {
diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index cc89073f8..c9cf8bfd2 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -69,7 +69,7 @@ namespace polysat {
             prop = true;
         if (try_transitivity(v, core, i))
             prop = true;
-        if (try_factor_equality1(v, core, i))
+        if (try_factor_equality2(v, core, i))
             prop = true;
         if (try_infer_equality(v, core, i))
             prop = true;
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 2e05c5b1d..1212d803a 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -172,9 +172,17 @@ namespace polysat {
 
         // NSB review:
         // the bounds added by x < p and p < x in forbidden_intervals
-        // match_non_max
+        // match_non_max, match_non_zero
         // use values that are approximations. Then the propagations in
         // try_assign_eval are incorrect.
+        // For example, x > p means x has forbidden interval [0, p + 1[,
+        // the numeric interval is [0, 1[, but p + 1 == 1 is not ensured
+        // even p may have free variables.
+        // the proper side condition on p + 1 is -1 > p or -2 >= p or p + 1 != 0
+        // I am disabling match_non_max and match_non_zero from forbidden_interval
+        // The narrowing rules in ule_constraint already handle the bounds propagaitons
+        // as it propagates p != -1 and 0 != q (p < -1, q > 0),
+        //
         
         for (auto const& c : get_constraints(v)) {
             s.try_assign_eval(c);