diff --git a/src/math/polysat/polysat.cpp b/src/math/polysat/polysat.cpp
index b8080cb93..cddbd8846 100644
--- a/src/math/polysat/polysat.cpp
+++ b/src/math/polysat/polysat.cpp
@@ -20,17 +20,17 @@ Author:
 namespace polysat {
 
     std::ostream& constraint::display(std::ostream& out) const {
-        return out << "constraint";
+        switch (kind()) {
+        case ckind_t::eq_t:
+            return out << p() << " == 0";
+        case ckind_t::ule_t:
+            return out << lhs() << " <=u " << rhs();
+        case ckind_t::sle_t:
+            return out << lhs() << " <=s " << rhs();
+        }
+        return out;
     }
     
-    std::ostream& linear::display(std::ostream& out) const {
-        return out << "linear";
-    }
-
-    std::ostream& mono::display(std::ostream& out) const {
-        return out << "mono";
-    }
-
     dd::pdd_manager& solver::sz2pdd(unsigned sz) {
         m_pdd.reserve(sz + 1);
         if (!m_pdd[sz])
@@ -128,7 +128,7 @@ namespace polysat {
         // TODO reduce p using assignment (at current level, 
         // assuming constraint is removed also at current level).
         // 
-        constraint* c = constraint::eq(p, m_dep_manager.mk_leaf(dep));
+        constraint* c = constraint::eq(m_level, p, m_dep_manager.mk_leaf(dep));
         m_constraints.push_back(c);
         auto const& vars = c->vars();
         if (vars.size() > 0) 
@@ -348,7 +348,7 @@ namespace polysat {
             if (r.is_val()) {
                 SASSERT(!r.is_zero());
                 // TBD: UNSAT, set conflict
-                return 0;
+                return i;
             }
             justification& j = m_justification[v];
             if (j.is_decision()) {
@@ -356,7 +356,7 @@ namespace polysat {
                 // propagate if new value is given uniquely
                 // set conflict if viable set is empty
                 // adding r and reverting last decision.
-                break;
+                break;                
             }
             SASSERT(j.is_propagation());
             for (auto w : r.free_vars())
@@ -423,6 +423,8 @@ namespace polysat {
     }
 
     std::ostream& solver::display(std::ostream& out) const {
+        for (auto* c : m_constraints)
+            out << *c << "\n";
         return out;
     }
 
diff --git a/src/math/polysat/polysat.h b/src/math/polysat/polysat.h
index a89941cea..9aed7cfcc 100644
--- a/src/math/polysat/polysat.h
+++ b/src/math/polysat/polysat.h
@@ -33,21 +33,26 @@ namespace polysat {
     enum ckind_t { eq_t, ule_t, sle_t };
 
     class constraint {
+        unsigned m_level;
         ckind_t m_kind;
         pdd    m_poly;
         pdd    m_other;
         u_dependency* m_dep;
         unsigned_vector m_vars;
-        constraint(pdd const& p, pdd const& q, u_dependency* dep, ckind_t k): 
-            m_kind(k), m_poly(p), m_other(q), m_dep(dep) {
+        constraint(unsigned lvl, pdd const& p, pdd const& q, u_dependency* dep, ckind_t k): 
+            m_level(lvl), m_kind(k), m_poly(p), m_other(q), m_dep(dep) {
             m_vars.append(p.free_vars());
             if (q != p) 
                 for (auto v : q.free_vars())
                     m_vars.insert(v);                
         }
     public:
-        static constraint* eq(pdd const& p, u_dependency* d) { return alloc(constraint, p, p, d, ckind_t::eq_t); }
-        static constraint* ule(pdd const& p, pdd const& q, u_dependency* d) { return alloc(constraint, p, q, d, ckind_t::ule_t); }
+        static constraint* eq(unsigned lvl, pdd const& p, u_dependency* d) { 
+            return alloc(constraint, lvl, p, p, d, ckind_t::eq_t); 
+        }
+        static constraint* ule(unsigned lvl, pdd const& p, pdd const& q, u_dependency* d) { 
+            return alloc(constraint, lvl, p, q, d, ckind_t::ule_t); 
+        }
         ckind_t kind() const { return m_kind; }
         pdd const &  p() const { return m_poly; }
         pdd const &  lhs() const { return m_poly; }
@@ -55,35 +60,11 @@ namespace polysat {
         std::ostream& display(std::ostream& out) const;
         u_dependency* dep() const { return m_dep; }
         unsigned_vector& vars() { return m_vars; }
+        unsigned level() const { return m_level; }
     };
 
     inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }
 
-    /**
-     * linear term is has an offset and is linear addition of variables.
-     */
-    class linear : public vector<std::pair<unsigned, rational>> {
-        rational m_offset;
-    public:
-        linear(rational const& offset): m_offset(offset) {}
-        rational const& offset() const { return m_offset; }
-        std::ostream& display(std::ostream& out) const;
-    };
-
-    inline std::ostream& operator<<(std::ostream& out, linear const& l) { return l.display(out); }
-
-    /**
-     * monomial is a list of variables and coefficient.
-     */
-    class mono : public unsigned_vector {
-        rational m_coeff;
-    public:
-        mono(rational const& coeff): m_coeff(coeff) {}
-        rational const& coeff() const { return m_coeff; }
-        std::ostream& display(std::ostream& out) const;
-    };
-
-    inline std::ostream& operator<<(std::ostream& out, mono const& m) { return m.display(out); }
 
     /**
      * Justification kind for a variable assignment.