diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index ff64be64b..52b21dd80 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3548,7 +3548,7 @@ namespace smt {
                 return false;
             }
             if (cmr == quantifier_manager::UNKNOWN) {
-                IF_VERBOSE(1, verbose_stream() << "(smt.giveup quantifiers)\n";);
+                IF_VERBOSE(2, verbose_stream() << "(smt.giveup quantifiers)\n";);
                 // giving up
                 m_last_search_failure = QUANTIFIERS;
                 status = l_undef;
@@ -3558,7 +3558,7 @@ namespace smt {
         inc_limits();
         if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) {
             SASSERT(!inconsistent());
-            IF_VERBOSE(1, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations 
+                IF_VERBOSE(2, verbose_stream() << "(smt.restarting :propagations " << m_stats.m_num_propagations 
                        << " :decisions " << m_stats.m_num_decisions
                        << " :conflicts " << m_stats.m_num_conflicts << " :restart " << m_restart_threshold;
                        if (m_fparams.m_restart_strategy == RS_IN_OUT_GEOMETRIC) {