diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index da702d4e3..7c9d2c965 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -1167,32 +1167,20 @@ namespace datalog {
         if (m_bmc) {
             m_bmc->reset_statistics();
         }
+        if (m_tab) {
+            m_tab->reset_statistics();
+        }
     }
 
     void context::collect_statistics(statistics& st) const {
-
-        switch(m_engine) {
-        case DATALOG_ENGINE: 
-            break;
-        case PDR_ENGINE: 
-        case QPDR_ENGINE:
-            if (m_pdr) {
-                m_pdr->collect_statistics(st);
-            }
-            break;
-        case BMC_ENGINE:
-        case QBMC_ENGINE:
-            if (m_bmc) {
-                m_bmc->collect_statistics(st);
-            }
-            break;
-        case TAB_ENGINE:
-            if (m_tab) {
-                m_tab->collect_statistics(st);
-            }
-            break;
-        default: 
-            break;
+        if (m_pdr) {
+            m_pdr->collect_statistics(st);
+        }
+        if (m_bmc) {
+            m_bmc->collect_statistics(st);
+        }
+        if (m_tab) {
+            m_tab->collect_statistics(st);
         }
     }
 
diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp
index 98b6130b8..0637148d6 100644
--- a/src/muz_qe/horn_tactic.cpp
+++ b/src/muz_qe/horn_tactic.cpp
@@ -240,6 +240,7 @@ class horn_tactic : public tactic {
     };
     
     params_ref m_params;
+    statistics m_stats;
     imp *      m_imp;
 public:
     horn_tactic(ast_manager & m, params_ref const & p):
@@ -272,20 +273,21 @@ public:
                             expr_dependency_ref & core) {
         (*m_imp)(in, result, mc, pc, core);
     }
-
     
     virtual void collect_statistics(statistics & st) const {
         m_imp->collect_statistics(st);
+        st.copy(m_stats);
     }
 
     virtual void reset_statistics() {
+        m_stats.reset();
         m_imp->reset_statistics();
     }
-
     
     virtual void cleanup() {
         ast_manager & m = m_imp->m;
         imp * d = m_imp;
+        d->collect_statistics(m_stats);
         #pragma omp critical (tactic_cancel)
         {
             m_imp = 0;