diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index 7b760d635ea..0478b878d7c 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -65,6 +65,7 @@ namespace smt {
         case CFG_LOGIC: setup_default(); break;
         case CFG_AUTO:  setup_auto_config(); break;
         }
+        setup_card();
     }
 
     void setup::setup_default() {
@@ -682,7 +683,6 @@ namespace smt {
         // 
         setup_mi_arith();
         setup_arrays(); 
-        setup_card();
     }
 
     void setup::setup_UFNIA() {
@@ -957,7 +957,6 @@ namespace smt {
         setup_recfuns();
         setup_dl();
         setup_seq_str(st);
-        setup_card();
         setup_fpa();
         if (st.m_has_sr) setup_special_relations();
     }
@@ -973,7 +972,6 @@ namespace smt {
             setup_bv();
             setup_dl();
             setup_seq_str(st);
-            setup_card();
             setup_fpa();
             setup_recfuns();
             if (st.m_has_sr) setup_special_relations();
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index 66631357e61..dd248bcca2f 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -41,7 +41,9 @@ struct tactic_report::imp {
     ~imp() {
         m_watch.stop();
         double end_memory = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024);
-        TRACE("tactic", m_goal.display(tout););
+        TRACE("tactic", m_goal.display(tout << m_id << "\n");
+              if (m_goal.mc()) m_goal.mc()->display(tout);
+              );
         IF_VERBOSE(0, 
                    verbose_stream() << "(" << m_id
                    << " :num-exprs " << m_goal.num_exprs()