diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 68d24d0a9..e358c5fe1 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2443,7 +2443,7 @@ bool ast_manager::is_pattern(expr const * n, ptr_vector<expr> &args) {
 
 static void trace_quant(std::ostream& strm, quantifier* q) {
     strm << (is_lambda(q) ? "[mk-lambda]" : "[mk-quant]")
-         << " #" << q->get_id() << " " << q->get_qid();
+         << " #" << q->get_id() << " " << q->get_qid() << " " << q->get_num_decls();
     for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
         strm << " #" << q->get_pattern(i)->get_id();
     }
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index c98cc06f8..4bc9b5170 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -461,6 +461,8 @@ namespace datatype {
                 func_decl_ref f = c->instantiate(new_sort);
                 const unsigned num_args = f->get_arity();
                 if (num_args == 0) continue;
+
+                // log constructor with quantified variables as arguments
                 for (unsigned i = 0; i < num_args; ++i) {
                     out << "[mk-var] " << family_name << "#" << m_id_counter << " " << i << "\n";
                     ++m_id_counter;
@@ -472,6 +474,8 @@ namespace datatype {
                 }
                 out << "\n";
                 ++m_id_counter;
+
+                // axioms for all accessors are generated when a constructor is applied => use constructor as pattern
                 out << "[mk-app] " << family_name << "#" << m_id_counter << " pattern " << family_name << "#" << constructor_id << "\n";
                 ++m_id_counter;
                 m_axiom_bases.insert(f->get_name(), constructor_id + 4);
@@ -480,6 +484,8 @@ namespace datatype {
                     var_sorts << " (;" << a->range()->get_name() << ")";
                 }
                 std::string var_description = var_sorts.str();
+
+                // create axioms: the ith accessor returns the ith argument of the constructor
                 unsigned i = 0;
                 for (accessor const* a : *c) {
                     func_decl_ref acc = a->instantiate(new_sort);
@@ -488,8 +494,8 @@ namespace datatype {
                     out << "[mk-app] " << family_name << "#" << m_id_counter << " = " << family_name << "#" << constructor_id - num_args + i 
                         << " " << family_name << "#" << m_id_counter - 1 << "\n";
                     ++m_id_counter;
-                    out << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << family_name << "#" << constructor_id + 1
-                        << " " << family_name << "#" << m_id_counter - 1 << "\n";
+                    out << "[mk-quant] " << family_name << "#" << m_id_counter << " constructor_accessor_axiom " << num_args << " " << family_name
+                        << "#" << constructor_id + 1 << " " << family_name << "#" << m_id_counter - 1 << "\n";
                     out << "[attach-var-names] " << family_name << "#" << m_id_counter << var_description << "\n";
                     ++m_id_counter;
                     ++i;
diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp
index d621a9f50..88d1f73e7 100644
--- a/src/smt/qi_queue.cpp
+++ b/src/smt/qi_queue.cpp
@@ -216,8 +216,10 @@ namespace smt {
         if (m_manager.is_true(s_instance)) {
             TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m_manager););
 
-            if (m_manager.has_trace_stream())
+            if (m_manager.has_trace_stream()) {
+                display_instance_profile(f, q, num_bindings, bindings, pr->get_id(), generation);
                 m_manager.trace_stream() << "[end-of-instance]\n";
+            }
 
             return;
         }