diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp
index ceb189486..b537a44dc 100644
--- a/src/smt/smt_clause_proof.cpp
+++ b/src/smt/smt_clause_proof.cpp
@@ -195,7 +195,6 @@ namespace smt {
         if (m_on_clause_eh) {
             // Encode status as an integer flag for simplicity.
             unsigned st_code = 0;
-            IF_VERBOSE(0, if (status::assumption != st) verbose_stream() << "status " << st << "\n");
             switch (st) {
                 case status::assumption:    st_code = 1; break;
                 case status::lemma:         st_code = 2; break;
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index c87ca6427..c0a2f3a4d 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -4386,8 +4386,6 @@ namespace smt {
                 }
             }
 #endif
-            IF_VERBOSE(0, verbose_stream() << "(smt.learned-clause"; verbose_stream() << " :size " << num_lits;
-                       verbose_stream() << " :conflicts " << m_num_conflicts << ")\n";);
             mk_clause(num_lits, lits, js, CLS_LEARNED);
             if (delay_forced_restart) {
                 SASSERT(num_lits == 1);
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 5777c3ed0..59c750306 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3469,7 +3469,6 @@ public:
     }
 
     void set_conflict_or_lemma(literal_vector const& core, bool is_conflict) {
-        IF_VERBOSE(0, verbose_stream() << "set conflict or lemma " << core << "\n");
         reset_evidence();
         for (literal lit : core) {
             m_core.push_back(lit);