diff --git a/src/math/polysat/umul_ovfl_constraint.cpp b/src/math/polysat/umul_ovfl_constraint.cpp
index ea7d28904..345541377 100644
--- a/src/math/polysat/umul_ovfl_constraint.cpp
+++ b/src/math/polysat/umul_ovfl_constraint.cpp
@@ -80,6 +80,9 @@ namespace polysat {
         if (is_always_true(is_positive, p1, q1))
             return;
 
+        if (first)
+            activate(s, is_positive);
+        
         if (try_viable(s, is_positive, p(), q(), p1, q1))
             return;
 
@@ -91,6 +94,16 @@ namespace polysat {
 
     }
 
+    void umul_ovfl_constraint::activate(solver& s, bool is_positive) {
+        // TODO - remove to enable
+        return;        
+        if (!is_positive) {
+            signed_constraint sc(this, is_positive);
+            s.add_clause(~sc, s.eq(p()), s.eq(q()), s.ule(p(), p()*q()), false);
+            s.add_clause(~sc, s.eq(p()), s.eq(q()), s.ule(q(), p()*q()), false);
+        }
+    }
+
     /**
      * if p constant, q, propagate inequality
      */
diff --git a/src/math/polysat/umul_ovfl_constraint.h b/src/math/polysat/umul_ovfl_constraint.h
index 1f2961f87..1595f0bd6 100644
--- a/src/math/polysat/umul_ovfl_constraint.h
+++ b/src/math/polysat/umul_ovfl_constraint.h
@@ -30,6 +30,7 @@ namespace polysat {
         static lbool eval(pdd const& p, pdd const& q);
         bool narrow_bound(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q);
         bool try_viable(solver& s, bool is_positive, pdd const& p0, pdd const& q0, pdd const& p, pdd const& q);
+        void activate(solver& s, bool is_positive);
 
     public:
         ~umul_ovfl_constraint() override {}