diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 6ebca4a3b..953b6fefa 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -320,12 +320,14 @@ namespace polysat {
         LOG_H3("Lemma: " << ": " << show_deref(lemma));
         VERIFY(lemma);
 
-        for (auto lit : *lemma)
-            if (s.m_bvars.is_true(lit)) {
-                verbose_stream() << "REDUNDANT lemma " << lit << " : " << show_deref(lemma) << "\n";
-                // for (sat::literal lit : *lemma)
-                //     verbose_stream() << "    " << lit_pp(s, lit) << "\n";
-            }
+        IF_VERBOSE(1, {
+            for (auto lit : *lemma)
+                if (s.m_bvars.is_true(lit)) {
+                    verbose_stream() << "REDUNDANT lemma " << lit << " : " << show_deref(lemma) << "\n";
+                    for (sat::literal lit : *lemma)
+                        verbose_stream() << "    " << lit_pp(s, lit) << "\n";
+                }
+        });
 
         s.m_simplify_clause.apply(*lemma);
         lemma->set_redundant(true);
diff --git a/src/math/polysat/restart.cpp b/src/math/polysat/restart.cpp
index 7d3b6a335..67fa82d5c 100644
--- a/src/math/polysat/restart.cpp
+++ b/src/math/polysat/restart.cpp
@@ -40,7 +40,7 @@ namespace polysat {
         s.pop_levels(s.m_level - s.base_level());
         m_conflicts_at_restart = s.m_stats.m_num_conflicts;
         m_restart_threshold = m_restart_init * get_luby(++m_luby_idx);
-        verbose_stream() << "Restart with Conflict #" << s.m_stats.m_num_conflicts << "\n";
+        IF_VERBOSE(10, verbose_stream() << "Restart with Conflict #" << s.m_stats.m_num_conflicts << "\n";);
         s.randomize_activity();
     }
 
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 819187190..401516525 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -470,12 +470,12 @@ namespace polysat {
             // <=> p * 2^(N - k) == 0
             if (k > N) {
                 // parity(p) > N is never true
-                verbose_stream() << "REDUNDANT parity constraint: parity_at_least(" << p << ", " << k << ")\n";
+                IF_VERBOSE(1, verbose_stream() << "REDUNDANT parity constraint: parity_at_least(" << p << ", " << k << ")\n";);
                 return ~eq(p.manager().zero());
             }
             else if (k == 0) {
                 // parity(p) >= 0 is a tautology
-                verbose_stream() << "REDUNDANT parity constraint: parity_at_least(" << p << ", " << k << ")\n";
+                IF_VERBOSE(1, verbose_stream() << "REDUNDANT parity constraint: parity_at_least(" << p << ", " << k << ")\n";);
                 return eq(p.manager().zero());
             }
             else if (k == N)
@@ -491,7 +491,7 @@ namespace polysat {
             // <=>  ~(parity(p) >= k+1)
             if (k >= N) {
                 // parity(p) <= N is a tautology
-                verbose_stream() << "REDUNDANT parity constraint: parity_at_most(" << p << ", " << k << ")\n";
+                IF_VERBOSE(1, verbose_stream() << "REDUNDANT parity constraint: parity_at_most(" << p << ", " << k << ")\n";);
                 return eq(p.manager().zero());
             }
             else
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index 5983cac16..af97ecb8d 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -1572,12 +1572,14 @@ namespace {
             else {
                 UNREACHABLE();
             }
-            if (refinements % 100 == 0)
-                verbose_stream() << "Refinements " << refinements << "\n";
+            IF_VERBOSE(10, {
+                if (refinements % 100 == 0)
+                    verbose_stream() << "Refinements " << refinements << "\n";
+            });
             if (res != l_undef)
                 return res;
         }
-        verbose_stream() << "Fallback\n";
+        IF_VERBOSE(10, verbose_stream() << "Fallback\n";);
         LOG("Refinement budget exhausted! Fall back to univariate solver.");
         return query_fallback<mode>(v, result);
     }
@@ -1730,7 +1732,6 @@ namespace {
                         added.insert(lit);
                         LOG("Adding " << lit_pp(s, lit));
                         IF_VERBOSE(10, verbose_stream() << ";; " << lit_pp(s, lit) << "\n");
-                        verbose_stream() << ";; " << lit_pp(s, lit) << "\n";
                         src.add_to_univariate_solver(v, s, *us, lit.to_uint());
                     }
                 }
@@ -1825,7 +1826,7 @@ namespace {
         }
         SASSERT(!core.vars().contains(v));
         core.add_lemma("viable unsat core", core.build_lemma());
-        verbose_stream() << "unsat core " << core << "\n";
+        IF_VERBOSE(10, verbose_stream() << "unsat core " << core << "\n";);
         return true;
     }