diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp
index 61f52ab59..655b5c2d7 100644
--- a/src/sat/smt/polysat/core.cpp
+++ b/src/sat/smt/polysat/core.cpp
@@ -392,7 +392,7 @@ namespace polysat {
         SASSERT(!is_assigned(v));
         if (!m_viable.assign(v, value, dep)) {
             auto deps = m_viable.explain();
-            verbose_stream() << "non-viable assignment v" << v << " == " << value << " <- " << deps << "\n";
+            TRACE("bv", tout << "non-viable assignment v" << v << " == " << value << " <- " << deps << "\n");
             s.set_conflict(deps, "non-viable assignment");
             return;
         }
diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index 1ed009593..8805903ce 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -207,7 +207,7 @@ namespace polysat {
             // display_explain(verbose_stream() << "found: ", {e,val}) << "\n";
             m_explain.push_back({ e, val });
             if (is_conflict()) {
-                verbose_stream() << "find_overlap conflict\n";
+                // verbose_stream() << "find_overlap conflict\n";
                 m_explain_kind = explain_t::conflict;
                 return nullptr;
             }