diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp
index cd56aea60..935bdced0 100644
--- a/src/ast/simplifiers/euf_completion.cpp
+++ b/src/ast/simplifiers/euf_completion.cpp
@@ -806,7 +806,6 @@ namespace euf {
 
     // callback when mam finds a binding
     void completion::on_binding(quantifier* q, app* pat, enode* const* binding, unsigned max_global, unsigned min_top, unsigned max_top) {
-        verbose_stream() << "on-binding\n";
         if (should_stop())
             return;
         if (max_top >= m_max_generation)
@@ -864,8 +863,6 @@ namespace euf {
             pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), r), s.size(), s.data());
         m_consequences.push_back(r);
         TRACE(euf_completion, tout << "new instantiation: " << r << " q: " << mk_pp(q, m) << "\n");
-        verbose_stream() << mk_pp(q, m) << " " << r
-                         << "\n ";
         add_constraint(r, pr, d);
         propagate_rules();
         m_egraph.propagate();