diff --git a/src/math/polysat/clause_builder.cpp b/src/math/polysat/clause_builder.cpp
index e3b504c77..2089b45fd 100644
--- a/src/math/polysat/clause_builder.cpp
+++ b/src/math/polysat/clause_builder.cpp
@@ -69,6 +69,7 @@ namespace polysat {
         if (c.is_always_false())  // filter out trivial constraints such as "4 < 2"
             return;
         if (c.is_always_true()) {
+            IF_VERBOSE(10, verbose_stream() << "Clause is tautology because of " << lit_pp(s(), c) << "\n");
             m_is_tautology = true;
             return;
         }
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index c262dd7c3..a5304e0fc 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -1121,6 +1121,7 @@ namespace {
             if (!added.contains(lit)) {
                 added.insert(lit);
                 LOG("Adding " << lit_pp(s, lit));
+                IF_VERBOSE(10, verbose_stream() << ";; " << lit_pp(s, lit) << "\n");
                 c.add_to_univariate_solver(v, s, *us, lit.to_uint());
             }
             e = e->next();
@@ -1147,6 +1148,7 @@ namespace {
             if (added.contains(lit))
                 continue;
             LOG("Adding " << lit_pp(s, lit));
+            IF_VERBOSE(10, verbose_stream() << ";; " << lit_pp(s, lit) << "\n");
             added.insert(lit);
             cs[i].add_to_univariate_solver(v, s, *us, lit.to_uint());
         }
@@ -1319,14 +1321,18 @@ namespace {
             log(v);
     }
 
-    std::ostream& viable::display(std::ostream& out, pvar v, entry* e) const {
+    std::ostream& viable::display_one(std::ostream& out, pvar v, entry const* e) const {
+        if (e->coeff != 1)
+            out << e->coeff << " * v" << v << " ";
+        out << e->interval << " " << e->side_cond << " " << e->src << "; ";
+        return out;
+    }
+    std::ostream& viable::display_all(std::ostream& out, pvar v, entry const* e) const {
         if (!e)
             return out;
-        entry* first = e;
+        entry const* first = e;
         do {
-            if (e->coeff != 1)
-                out << e->coeff << " * v" << v << " ";
-            out << e->interval << " " << e->side_cond << " " << e->src << "; ";
+            display_one(out, v, e);
             e = e->next();
         }
         while (e != first);
@@ -1334,9 +1340,9 @@ namespace {
     }
 
     std::ostream& viable::display(std::ostream& out, pvar v) const {
-        display(out, v, m_units[v]);
-        display(out, v, m_equal_lin[v]);
-        display(out, v, m_diseq_lin[v]);
+        display_all(out, v, m_units[v]);
+        display_all(out, v, m_equal_lin[v]);
+        display_all(out, v, m_diseq_lin[v]);
         return out;
     }
 
diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h
index 68dab9d77..475df101a 100644
--- a/src/math/polysat/viable.h
+++ b/src/math/polysat/viable.h
@@ -40,6 +40,8 @@ namespace polysat {
         resource_out,
     };
 
+    std::ostream& operator<<(std::ostream& out, find_t x);
+
     namespace viable_query {
         enum class query_t {
             has_viable,  // currently only used internally in resolve_viable
@@ -68,8 +70,6 @@ namespace polysat {
         };
     }
 
-    std::ostream& operator<<(std::ostream& out, find_t x);
-
     class viable {
         friend class test_fi;
 
@@ -99,7 +99,8 @@ namespace polysat {
 
         bool refine_disequal_lin(pvar v, rational const& val);
 
-        std::ostream& display(std::ostream& out, pvar v, entry* e) const;
+        std::ostream& display_one(std::ostream& out, pvar v, entry const* e) const;
+        std::ostream& display_all(std::ostream& out, pvar v, entry const* e) const;
 
         void insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k);