diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp
index 94e159f4f..899e3f031 100644
--- a/src/math/polysat/constraint.cpp
+++ b/src/math/polysat/constraint.cpp
@@ -82,6 +82,10 @@ namespace polysat {
         return { std::move(lhs), std::move(rhs), m_src };
     }
 
+    std::ostream& inequality::display(std::ostream& out) const {
+        return out << m_lhs << (is_strict() ? " < " : " <= ") << m_rhs;
+    }
+
     pdd const& constraint::to_eq() const {
         SASSERT(is_eq());
         return to_ule().lhs();
diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h
index c5ce2c2aa..8c96926a5 100644
--- a/src/math/polysat/constraint.h
+++ b/src/math/polysat/constraint.h
@@ -236,6 +236,8 @@ namespace polysat {
          *      i=5     -q - 1 <= p - q - 1
          */
         inequality rewrite_equiv(int i) const;
+
+        std::ostream& display(std::ostream& out) const;
     };
 
     class constraint_pp {
@@ -248,6 +250,6 @@ namespace polysat {
 
     inline std::ostream& operator<<(std::ostream& out, constraint_pp const& p) { return p.display(out); }
 
-    inline std::ostream& operator<<(std::ostream& out, inequality const& i) { return out << i.as_signed_constraint(); }
+    inline std::ostream& operator<<(std::ostream& out, inequality const& i) { return i.display(out); }
 
 }