diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 353cc820a..9b4c4e555 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -34,49 +34,9 @@ namespace polysat {
         return *m_pdd[sz];
     }
 
-#if 0
-    dd::fdd const& solver::sz2bits(unsigned sz) {
-        m_bits.reserve(sz + 1);
-        auto* bits = m_bits[sz];
-        if (!bits) {
-            m_bits.set(sz, alloc(dd::fdd, m_bdd, sz));
-            bits = m_bits[sz];
-        }
-        return *bits;
-    }
-
-    bool solver::has_viable(pvar v) {
-        return !m_viable[v].is_false();
-    }
-
-    bool solver::is_viable(pvar v, rational const& val) {
-        return var2bits(v).contains(m_viable[v], val);
-    }
-
-    void solver::add_non_viable(pvar v, rational const& val) {
-        LOG("pvar " << v << " /= " << val);
-        SASSERT(is_viable(v, val));
-        auto const& bits = var2bits(v);
-        intersect_viable(v, bits.var() != val);
-    }
-
-    void solver::intersect_viable(pvar v, bdd vals) {
-        push_viable(v);
-        m_viable[v] &= vals;
-        if (m_viable[v].is_false())
-            set_conflict(v);
-    }
-
-    dd::find_t solver::find_viable(pvar v, rational & val) {
-        return var2bits(v).find_hint(m_viable[v], m_value[v], val);
-    }
-    
-#endif
-
     solver::solver(reslimit& lim): 
         m_lim(lim),
         m_vble(*this),
-        // m_bdd(1000),
         m_dm(m_value_manager, m_alloc),
         m_linear_solver(*this),
         m_free_vars(m_activity),
diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp
index 5be78e30d..ec2538b56 100644
--- a/src/math/polysat/ule_constraint.cpp
+++ b/src/math/polysat/ule_constraint.cpp
@@ -74,24 +74,13 @@ namespace polysat {
             d = q.lo().val();
         }
         if (v != null_var) {
-            bddv const& x = s.m_vble.var2bits(v).var();
             s.push_cjust(v, this);
-            // hacky special case
-            if (a == 1 && b == 0 && c == 0 && d == 0) 
-                // x <= 0
-                s.m_vble.intersect_viable(v, is_positive() ? x.all0() : !x.all0());
-            else {
-                IF_VERBOSE(10, verbose_stream() << a << "*x + " << b << (is_positive() ? " <= " : " > ") << c << "*x + " << d << "\n");
-                bddv l = a * x + b;
-                bddv r = c * x + d;
-                bdd xs = is_positive() ? (l <= r) : (l > r);
-                s.m_vble.intersect_viable(v, xs);
-            }
+
+            s.m_vble.intersect_ule(v, a, b, c, d, is_positive());
 
             rational val;
-            if (s.m_vble.find_viable(v, val) == dd::find_t::singleton) {
+            if (s.m_vble.find_viable(v, val) == dd::find_t::singleton) 
                 s.propagate(v, val, *this);
-            }
 
             return;
         }
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index c8efc2361..dfa92f877 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -46,6 +46,21 @@ namespace polysat {
         }
     }
 
+    void viable::intersect_ule(pvar v, rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive) {
+        bddv const& x = var2bits(v).var();
+        // hacky special case
+        if (a == 1 && b == 0 && c == 0 && d == 0) 
+            // x <= 0
+            intersect_viable(v, is_positive ? x.all0() : !x.all0());
+        else {
+            IF_VERBOSE(10, verbose_stream() << a << "*x + " << b << (is_positive ? " <= " : " > ") << c << "*x + " << d << "\n");
+            bddv l = a * x + b;
+            bddv r = c * x + d;
+            bdd xs = is_positive ? (l <= r) : (l > r);
+            intersect_viable(v, xs);
+        }
+    }
+
     bool viable::has_viable(pvar v) {
         return !m_viable[v].is_false();
     }
diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h
index 3cc1d6fe5..c893bf051 100644
--- a/src/math/polysat/viable.h
+++ b/src/math/polysat/viable.h
@@ -42,6 +42,8 @@ namespace polysat {
 
         void intersect_eq(rational const& a, pvar v, rational const& b, bool is_positive);
 
+        void intersect_ule(pvar v, rational const& a, rational const& b, rational const& c, rational const& d, bool is_positive);
+
         /**
          * Check whether variable v has any viable values left according to m_viable.
          */