diff --git a/src/sat/smt/q_queue.cpp b/src/sat/smt/q_queue.cpp
index c30009127..ff7dbc8ab 100644
--- a/src/sat/smt/q_queue.cpp
+++ b/src/sat/smt/q_queue.cpp
@@ -163,12 +163,13 @@ namespace q {
 
         m_stats.m_num_instances++;
 
+#if 0
         std::cout << "instantiate\n";
         for (unsigned i = 0; i < num_bindings; ++i)
             std::cout << ctx.bpp(f[i]) << " ";
         std::cout << "\n";
         std::cout << mk_pp(q, m) << "\n";
-
+#endif
 
 //        f.display(ctx, std::cout << mk_pp(f.q(), m) << "\n" << instance << "\n") <<  "\n";
 
diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp
index 7c21c1362..1cef2a0f1 100644
--- a/src/smt/qi_queue.cpp
+++ b/src/smt/qi_queue.cpp
@@ -245,13 +245,15 @@ namespace smt {
 
             return;
         }
+#if 0
         std::cout << "instantiate\n";
         enode_vector _bindings(num_bindings, bindings);
         for (auto * b : _bindings)
             std::cout << enode_pp(b, m_context) << " ";
         std::cout << "\n";
         std::cout << mk_pp(q, m) << "\n";
-        
+#endif
+   
         TRACE("qi_queue", tout << "simplified instance:\n" << s_instance << "\n";);
         stat->inc_num_instances();
         if (stat->get_num_instances() % m_params.m_qi_profile_freq == 0) {