diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 05e699a22..5b6719450 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -80,11 +80,11 @@ namespace polysat {
                     m_used_vars.insert(v);
             }
             for (auto v : core.vars()) {
-                out_indent() << "v" << v << " := " << core.s.get_value(v) << "\n";
+                out_indent() << assignment_pp(core.s, v, core.s.get_value(v)) << "\n";
                 m_used_vars.insert(v);
             }
             for (auto v : core.bail_vars()) {
-                out_indent() << "v" << v << " := " << core.s.get_value(v) << " (bail)\n";
+                out_indent() << assignment_pp(core.s, v, core.s.get_value(v)) << " (bail)\n";
                 m_used_vars.insert(v);
             }
             if (core.is_bailout())
diff --git a/src/math/polysat/search_state.cpp b/src/math/polysat/search_state.cpp
index 399bb2e1e..637cfff63 100644
--- a/src/math/polysat/search_state.cpp
+++ b/src/math/polysat/search_state.cpp
@@ -21,22 +21,17 @@ namespace polysat {
     std::ostream& search_state::display_verbose(search_item const& item, std::ostream& out) const {
         switch (item.kind()) {
         case search_item_k::assignment: {
-            rational r;
-            pvar const v = item.var();
-            auto const& j = s.m_justification[v];
-            out << "v" << std::setw(3) << std::left << v << " := ";
-            out << std::setw(30) << std::left << s.m_value[v];
-            // if (value(item.var(), r)) {
-            //     SASSERT_EQ(r, s.m_value[v]);
-            //     out << r;
-            // } else
-            //     out << "*";
+            pvar const var = item.var();
+            rational const& val = s.m_value[var];
+            auto const& j = s.m_justification[var];
+            out << "v" << std::setw(3) << std::left << var << " := ";
+            out << std::setw(30) << std::left << num_pp(s, var, val);
             out << " @" << j.level();
             switch (j.kind()) {
             case justification_k::decision:
                 return out << " by decision";
             case justification_k::propagation:
-                return out << " by " << viable::var_pp(s.m_viable, v);
+                return out << " by " << viable::var_pp(s.m_viable, var);
             case justification_k::unassigned:
                 return out << " unassigned";
             }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index f0b47065b..795a10dec 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1185,17 +1185,20 @@ namespace polysat {
     }
 
     std::ostream& assignment_pp::display(std::ostream& out) const {
-        out << "v" << var << " := ";
+        out << "v" << var << " := " << num_pp(s, var, val);
+        if (with_justification)
+            out << " (" << s.m_justification[var] << ")";
+        return out;
+    }
+
+    std::ostream& num_pp::display(std::ostream& out) const {
         rational const& p = rational::power_of_two(s.size(var));
         if (val > mod(-val, p))
             out << -mod(-val, p);
         else 
             out << val;
-        if (with_justification)
-            out << " (" << s.m_justification[var] << ")";
         return out;
     }
-    
 
     void solver::collect_statistics(statistics& st) const {
         st.update("polysat iterations",   m_stats.m_num_iterations);
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 5192cf4bd..ff5e3d8b9 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -78,6 +78,7 @@ namespace polysat {
         friend class viable;
         friend class viable_fallback;
         friend class search_state;
+        friend class num_pp;
         friend class assignment_pp;
         friend class assignments_pp;
         friend class ex_polynomial_superposition;
@@ -429,12 +430,25 @@ namespace polysat {
         std::ostream& display(std::ostream& out) const;
     };
 
+    /** Format value 'val' as member of the domain of 'var' */
+    class num_pp {
+        solver const& s;
+        pvar var;
+        rational const& val;
+    public:
+        num_pp(solver const& s, pvar var, rational const& val): s(s), var(var), val(val) {}
+        std::ostream& display(std::ostream& out) const;
+    };
+
     inline std::ostream& operator<<(std::ostream& out, solver const& s) { return s.display(out); }
 
+    inline std::ostream& operator<<(std::ostream& out, num_pp const& v) { return v.display(out); }
+
     inline std::ostream& operator<<(std::ostream& out, assignment_pp const& p) { return p.display(out); }
 
     inline std::ostream& operator<<(std::ostream& out, assignments_pp const& a) { return a.display(out); }
 
+
 }