diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 74166a78b..5fcc8d63b 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2369,6 +2369,15 @@ bool ast_manager::is_pattern(expr const * n, ptr_vector<expr> &args) {
     return true;
 }
 
+static void trace_quant(std::ostream& strm, quantifier* q) {
+    strm << (is_lambda(q) ? "[mk-lambda]" : "[mk-quant]")
+         << " #" << q->get_id() << " " << q->get_qid();
+    for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
+        strm << " #" << q->get_pattern(i)->get_id();
+    }
+    strm << " #" << q->get_expr()->get_id() << "\n";
+}
+
 
 quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names,
                                         expr * body, int weight , symbol const & qid, symbol const & skid,
@@ -2401,11 +2410,7 @@ quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, s
     quantifier * r = register_node(new_node);
 
     if (m_trace_stream && r == new_node) {
-        *m_trace_stream << "[mk-quant] #" << r->get_id() << " " << qid;
-        for (unsigned i = 0; i < num_patterns; ++i) {
-            *m_trace_stream << " #" << patterns[i]->get_id();
-        }
-        *m_trace_stream << " #" << body->get_id() << "\n";
+        trace_quant(*m_trace_stream, r);
     }
 
     return r;
@@ -2420,7 +2425,7 @@ quantifier * ast_manager::mk_lambda(unsigned num_decls, sort * const * decl_sort
     quantifier * new_node = new (mem) quantifier(num_decls, decl_sorts, decl_names, body, s);
     quantifier * r = register_node(new_node);
     if (m_trace_stream && r == new_node) {
-        *m_trace_stream << "[mk-lambda] #" << r->get_id() << ": #" << body->get_id() << "\n";
+        trace_quant(*m_trace_stream, r);
     }
     return r;
 }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index d6937aa79..8f64544b4 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -4581,7 +4581,6 @@ bool theory_seq::lower_bound(expr* _e, rational& lo) const {
         if (thi && thi->get_lower(ctx.get_enode(e), _lo)) break;
         theory_lra* thr = get_th_arith<theory_lra>(ctx, afid, e);
         if (thr && thr->get_lower(ctx.get_enode(e), _lo)) break;
-        TRACE("seq", tout << "no lower bound " << mk_pp(_e, m) << "\n";);
         return false;
     }
     while (false);
@@ -4639,7 +4638,6 @@ bool theory_seq::upper_bound(expr* _e, rational& hi) const {
         if (thi && thi->get_upper(ctx.get_enode(e), _hi)) break;
         theory_lra* thr = get_th_arith<theory_lra>(ctx, afid, e);
         if (thr && thr->get_upper(ctx.get_enode(e), _hi)) break;
-        TRACE("seq", tout << "no upper bound " << mk_pp(_e, m) << "\n";);
         return false;
     }
     while (false);