diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 305d91c97..ab37a9f40 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2477,6 +2477,11 @@ quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, s
 
     if (m_trace_stream && r == new_node) {
         trace_quant(*m_trace_stream, r);
+        *m_trace_stream << "[attach-var-names] #" << r->get_id();
+        for (unsigned i = 0; i < num_decls; ++i) {
+            *m_trace_stream << " " << decl_names[num_decls - i - 1].str();
+        }
+        *m_trace_stream << "\n";
     }
 
     return r;
diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 7098f2d9c..a22889b24 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -212,7 +212,7 @@ namespace smt {
             if (f) {
                 if (has_trace_stream()) {
                     if (pat == nullptr) {
-                        trace_stream() << "[mbqi-triggered] " << static_cast<void*>(f) << " #" << q->get_id();
+                        trace_stream() << "[inst-possible] MBQI " << static_cast<void*>(f) << " #" << q->get_id();
                         for (unsigned i = 0; i < num_bindings; ++i) {
                             trace_stream() << " #" << bindings[num_bindings - i - 1]->get_owner_id();
                         }