diff --git a/src/math/polysat/saturation.cpp b/src/math/polysat/saturation.cpp
index e89b63e76..780a9a7e4 100644
--- a/src/math/polysat/saturation.cpp
+++ b/src/math/polysat/saturation.cpp
@@ -1245,6 +1245,8 @@ namespace polysat {
         for (auto c : core) {
             if (!c->is_ule())
                 continue;
+            if (c->to_ule().power_of_2() != m.power_of_2())
+                continue;
             auto i = inequality::from_ule(c);
             if (c == a_l_b.as_signed_constraint())
                 continue;
diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp
index 20e4c260f..0ef575d5b 100644
--- a/src/math/polysat/ule_constraint.cpp
+++ b/src/math/polysat/ule_constraint.cpp
@@ -194,6 +194,8 @@ namespace polysat {
     ule_constraint::ule_constraint(pdd const& l, pdd const& r) :
         constraint(ckind_t::ule_t), m_lhs(l), m_rhs(r) {
 
+        SASSERT_EQ(m_lhs.power_of_2(), m_rhs.power_of_2());
+
         m_vars.append(m_lhs.free_vars());
         for (auto v : m_rhs.free_vars())
             if (!m_vars.contains(v))
@@ -201,6 +203,7 @@ namespace polysat {
     }
 
     void ule_constraint::simplify(bool& is_positive, pdd& lhs, pdd& rhs) {
+        SASSERT_EQ(lhs.power_of_2(), rhs.power_of_2());
 #ifndef NDEBUG
         bool const old_is_positive = is_positive;
         pdd const old_lhs = lhs;
diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h
index ed0ba2c8c..d721b420c 100644
--- a/src/math/polysat/ule_constraint.h
+++ b/src/math/polysat/ule_constraint.h
@@ -45,6 +45,7 @@ namespace polysat {
         bool operator==(constraint const& other) const override;
         bool is_eq() const override { return m_rhs.is_zero(); }
         void add_to_univariate_solver(pvar v, solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
+        unsigned power_of_2() const { return m_lhs.power_of_2(); }
     };
 
     struct ule_pp {