diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index b1609ed85..8bf6efac5 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -75,6 +75,18 @@ void report_tactic_progress(char const * id, unsigned val) {
     }
 }
 
+statistics_report::~statistics_report() {
+    statistics st;
+    if (m_tactic)
+        m_tactic->collect_statistics(st);
+    else if (m_collector)
+        m_collector(st);
+    if (st.size() == 0)
+        return;
+    IF_VERBOSE(TACTIC_VERBOSITY_LVL, st.display_smt2(verbose_stream()));
+}
+
+
 void skip_tactic::operator()(goal_ref const & in, goal_ref_buffer& result) {
     result.push_back(in.get());
 }
diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h
index 0f55ea0fe..c43120943 100644
--- a/src/tactic/tactic.h
+++ b/src/tactic/tactic.h
@@ -115,6 +115,15 @@ public:
 
 void report_tactic_progress(char const * id, unsigned val);
 
+class statistics_report {
+    tactic* m_tactic = nullptr;
+    std::function<void(statistics& st)> m_collector;
+public:
+    statistics_report(tactic& t):m_tactic(&t) {}
+    statistics_report(std::function<void(statistics&)>& coll): m_collector(coll) {}
+    ~statistics_report();
+};
+
 class skip_tactic : public tactic {
 public:
     void operator()(goal_ref const & in, goal_ref_buffer& result) override;