diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp
index d12af572b..a0024c9ec 100644
--- a/src/math/polysat/ule_constraint.cpp
+++ b/src/math/polysat/ule_constraint.cpp
@@ -49,7 +49,15 @@ namespace polysat {
     ule_constraint::ule_constraint(constraint_manager& m, pdd const& l, pdd const& r) :
         constraint(m, ckind_t::ule_t), m_lhs(l), m_rhs(r) {
 
+#ifndef NDEBUG
+        pdd const old_lhs = m_lhs;
+        pdd const old_rhs = m_rhs;
+#endif
         simplify();
+#ifndef NDEBUG
+        if (old_lhs != m_lhs || old_rhs != m_rhs)
+            LOG("Simplify: " << ule_pp(l_true, old_lhs, old_rhs) << "   -->   " << ule_pp(l_true, m_lhs, m_rhs));
+#endif
 
         m_vars.append(m_lhs.free_vars());
         for (auto v : m_rhs.free_vars())
@@ -96,14 +104,20 @@ namespace polysat {
         }
     }
 
-    std::ostream& ule_constraint::display(std::ostream& out, lbool status) const {
-        out << m_lhs;
-        if (is_eq() && status == l_true) out << " == ";
-        else if (is_eq() && status == l_false) out << " != ";
+    std::ostream& ule_constraint::display(std::ostream& out, lbool status, pdd const& lhs, pdd const& rhs) {
+        out << lhs;
+        if (rhs.is_zero() && status == l_true) out << " == ";
+        else if (rhs.is_zero() && status == l_false) out << " != ";
+        // else if (lhs.is_one() && status == l_true) out << " != ";
+        // else if (lhs.is_one() && status == l_false) out << " == ";
         else if (status == l_true) out << " <= ";
         else if (status == l_false) out << " > ";
         else out << " <=/> ";
-        return out << m_rhs;
+        return out << rhs;
+    }
+
+    std::ostream& ule_constraint::display(std::ostream& out, lbool status) const {
+        return display(out, status, m_lhs, m_rhs);
     }
 
     std::ostream& ule_constraint::display(std::ostream& out) const {
diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h
index 87d74859d..4fb518efb 100644
--- a/src/math/polysat/ule_constraint.h
+++ b/src/math/polysat/ule_constraint.h
@@ -32,6 +32,7 @@ namespace polysat {
         ~ule_constraint() override {}
         pdd const& lhs() const { return m_lhs; }
         pdd const& rhs() const { return m_rhs; }
+        static std::ostream& display(std::ostream& out, lbool status, pdd const& lhs, pdd const& rhs);
         std::ostream& display(std::ostream& out, lbool status) const override;
         std::ostream& display(std::ostream& out) const override;
         static bool is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs);
@@ -49,4 +50,13 @@ namespace polysat {
         void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const override;
     };
 
+    struct ule_pp {
+        lbool status;
+        pdd lhs;
+        pdd rhs;
+        ule_pp(lbool status, pdd const& lhs, pdd const& rhs): status(status), lhs(lhs), rhs(rhs) {}
+    };
+
+    inline std::ostream& operator<<(std::ostream& out, ule_pp const& u) { return ule_constraint::display(out, u.status, u.lhs, u.rhs); }
+
 }