diff --git a/src/sat/smt/polysat/assignment.cpp b/src/sat/smt/polysat/assignment.cpp
index c1620891a..c67b681de 100644
--- a/src/sat/smt/polysat/assignment.cpp
+++ b/src/sat/smt/polysat/assignment.cpp
@@ -102,7 +102,7 @@ namespace polysat {
     std::ostream& assignment::display(std::ostream& out) const {
         char const* delim = "";
         for (auto const& [var, value] : m_pairs) 
-            out << delim << var << " == " << value, delim = " ";	  
+            out << delim << "v" << var << " == " << value, delim = " ";
         return out;
     }
 }
diff --git a/src/sat/smt/polysat/ule_constraint.cpp b/src/sat/smt/polysat/ule_constraint.cpp
index 0d9923836..35dc3f6f4 100644
--- a/src/sat/smt/polysat/ule_constraint.cpp
+++ b/src/sat/smt/polysat/ule_constraint.cpp
@@ -136,7 +136,7 @@ namespace polysat {
         }
 
         if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs.val()) {
-            TRACE("bv", tout << "- p + k <= k-->  p <= k\n");
+            TRACE("bv", tout << "- p + k <= k     -->  p <= k\n");
             lhs = rhs - lhs;
         }
 
@@ -148,7 +148,7 @@ namespace polysat {
         }
 
         if (lhs.is_val() && rhs.leading_coefficient().get_bit(N - 1) && !rhs.offset().is_zero()) {
-            TRACE("bv", tout << "k <= -p-->  p - 1 <= -k - 1\n");
+            TRACE("bv", tout << "k <= -p          -->  p - 1 <= -k - 1\n");
             pdd k = lhs;
             lhs = -(rhs + 1);
             rhs = -k - 1;