diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 1a6a0fe90..1e117e9ff 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -472,9 +472,14 @@ namespace polysat {
         if (is_bailout())
             goto bailout;
         
-        if (j.is_propagation()) 
+        if (j.is_propagation()) {
             for (auto const& c : s.m_viable.get_constraints(v)) 
                 propagate(c);
+            for (auto const& i : s.m_viable.units(v)) {
+                propagate(s.eq(i.lo(), i.lo_val()));
+                propagate(s.eq(i.hi(), i.hi_val()));                   
+            }                
+        }
 
         LOG("try-explain v" << v);
         if (try_explain(v))
diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h
index cffc4f14e..e972e0e05 100644
--- a/src/math/polysat/viable.h
+++ b/src/math/polysat/viable.h
@@ -168,6 +168,43 @@ namespace polysat {
             return constraints(*this, v); 
         }
 
+        class int_iterator {
+            entry* curr = nullptr;
+            bool visited = false;
+        public:
+            int_iterator(entry* curr, bool visited) :
+                curr(curr), visited(visited || !curr) {}
+            int_iterator& operator++() {
+                visited = true;
+                curr = curr->next();
+                return *this;
+            }
+
+            eval_interval const& operator*() { 
+                return curr->interval;                
+            }
+
+            bool operator==(int_iterator const& other) const {
+                return visited == other.visited && curr == other.curr;
+            }
+
+            bool operator!=(int_iterator const& other) const {
+                return !(*this == other);
+            }
+
+        };
+
+        class intervals {
+            viable const& v;
+            pvar var;
+        public:
+            intervals(viable const& v, pvar var): v(v), var(var) {}
+            int_iterator begin() const { return int_iterator(v.m_units[var], false); }
+            int_iterator end() const { return int_iterator(v.m_units[var], true); }
+        };
+
+        intervals units(pvar v) { return intervals(*this, v); }
+
         std::ostream& display(std::ostream& out, pvar v) const;
 
         struct var_pp {