diff --git a/src/sat/smt/polysat/inequality.h b/src/sat/smt/polysat/inequality.h
index 563cca4cc..e712c9afb 100644
--- a/src/sat/smt/polysat/inequality.h
+++ b/src/sat/smt/polysat/inequality.h
@@ -100,13 +100,14 @@ namespace polysat {
         bool verify_YX_l_zX(pvar z, pdd const& x, pdd const& y) const;
 
         // c := xY <= xZ
-        bool is_xY_l_xZ(pvar x, pdd& y, pdd& z) const { return is_xY(x, lhs(), y) && is_xY(x, rhs(), z); }
+        bool is_xY_l_xZ(pvar x, pdd& y, pdd& z) const { return is_xY_2(x, lhs(), y) && is_xY_2(x, rhs(), z); }
 
-        /**
-         * Match xy = x * Y
-        */
+        /// Match xy = x * Y s.t. Y is free of x
         static bool is_xY(pvar x, pdd const& xy, pdd& y) { return xy.degree(x) == 1 && xy.factor(x, 1, y); }
 
+        /// Match xy = x * Y
+        static bool is_xY_2(pvar x, pdd const& xy, pdd& y) { return xy.factor(x, 1, y); }
+
         /**
          * Rewrite to one of six equivalent forms:
          *
@@ -165,7 +166,7 @@ namespace polysat {
             r.d -= d;
             return r;
         }
-};
+    };
 
     inline std::ostream& operator<<(std::ostream& out, bilinear const& b) {
         return out << b.a << "*x*y + " << b.b << "*x + " << b.c << "*y + " << b.d;
diff --git a/src/sat/smt/polysat/saturation.cpp b/src/sat/smt/polysat/saturation.cpp
index 8a21c873b..69be7c22f 100644
--- a/src/sat/smt/polysat/saturation.cpp
+++ b/src/sat/smt/polysat/saturation.cpp
@@ -118,22 +118,48 @@ namespace polysat {
 
     /**
      * Implement the inferences
-     *  [x] yx < zx   ==>  Ω*(x,y) \/ y < z
-     *  [x] yx <= zx  ==>  Ω*(x,y) \/ y <= z \/ x = 0
+     *  [x] px < qx   ==>  p != q
+     *  [x] px < qx   ==>  Ω*(p,x) \/ p < q
+     *  [x] px < qx   ==>  Ω*(-q,x) \/ p < q
+     *  [x] px < qx   ==>  Ω*(q,-x) \/ p > q \/ p = 0
+     *  [x] px < qx   ==>  Ω*(-p,-x) \/ p > q \/ p = 0
+     *
+     *  [x] px <= qx  ==>  Ω*(p,x) \/ p <= q \/ x = 0
+     *  [x] px <= qx  ==>  Ω*(-q,x) \/ p <= q \/ x = 0 \/ q = 0
+     *  [x] px <= qx  ==>  Ω*(q,-x) \/ p >= q \/ x = 0 \/ p = 0
+     *  [x] px <= qx  ==>  Ω*(-p,-x) \/ p >= q \/ x = 0 \/ p = 0
      */
     void saturation::try_ugt_x(pvar v, inequality const& i) {
         pdd x = c.var(v);
-        pdd y = x;
-        pdd z = x;       
+        pdd p = x;
+        pdd q = x;
+        auto const& d = i.dep();
 
-        if (!i.is_xY_l_xZ(v, y, z))
+        if (!i.is_xY_l_xZ(v, p, q))
             return;
 
-        auto ovfl = C.umul_ovfl(x, y);
-        if (i.is_strict()) 
-            add_clause("[x] yx < zx ==> Ω*(x,y) \\/ y < z", { i.dep(), ovfl, C.ult(y, z)}, true);
-        else 
-            add_clause("[x] yx <= zx ==> Ω*(x,y) \\/ y <= z \\/ x = 0", { i.dep(), ovfl, C.eq(x), C.ule(y, z) }, true);
+        if (i.is_strict()) {
+            if (!c.inconsistent())
+                add_clause("[x] px < qx ==> p != q", { d, C.diseq(p, q) });
+            if (!c.inconsistent())
+                add_clause("[x] px < qx ==> Ω*(p,x) \\/ p < q", { d, C.umul_ovfl(p, x), C.ult(p, q) });
+            if (!c.inconsistent())
+                add_clause("[x] px < qx ==> Ω*(-q,x) \\/ p < q", { d, C.umul_ovfl(-q, x), C.ult(p, q) });
+            if (!c.inconsistent())
+                add_clause("[x] px < qx ==> Ω*(q,-x) \\/ p > q \\/ p = 0", { d, C.umul_ovfl(q, -x), C.ugt(p, q), C.eq(p) });
+            if (!c.inconsistent())
+                add_clause("[x] px < qx ==> Ω*(-p,-x) \\/ p > q \\/ p = 0", { d, C.umul_ovfl(-p, -x), C.ugt(p, q), C.eq(p) });
+        }
+        else {
+            if (!c.inconsistent())
+                add_clause("[x] px <= qx ==> Ω*(p,x) \\/ p <= q \\/ x = 0", { d, C.umul_ovfl(p, x), C.eq(x), C.ule(p, q) });
+            if (!c.inconsistent())
+                add_clause("[x] px <= qx ==> Ω*(-q,x) \\/ p <= q \\/ x = 0 \\/ q = 0", { d, C.umul_ovfl(-q, x), C.eq(x), C.eq(q), C.ule(p, q) });
+            if (!c.inconsistent())
+                add_clause("[x] px <= qx ==> Ω*(q,-x) \\/ p >= q \\/ x = 0 \\/ p = 0", { d, C.umul_ovfl(q, -x), C.eq(x), C.eq(p), C.uge(p, q) });
+            if (!c.inconsistent())
+                add_clause("[x] px <= qx ==> Ω*(-p,-x) \\/ p >= q \\/ x = 0 \\/ p = 0", { d, C.umul_ovfl(-p, -x), C.eq(x), C.eq(p), C.uge(p, q) });
+        }
     }
 
     /**
diff --git a/src/sat/smt/polysat/saturation.h b/src/sat/smt/polysat/saturation.h
index e2d899792..4dbd5ede0 100644
--- a/src/sat/smt/polysat/saturation.h
+++ b/src/sat/smt/polysat/saturation.h
@@ -29,7 +29,7 @@ namespace polysat {
         core& c;
         constraints& C;
 
-        void add_clause(char const* name, clause const& cs, bool is_redundant);
+        void add_clause(char const* name, clause const& cs, bool is_redundant = true);
 
         struct constraint_filter {
             core& c;