1 files changed, 11 insertions, 0 deletions
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index 1dd69abc9..83da5a159 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -73,7 +73,18 @@ public:
     s_smtEngine_current = d_oldSmtEngine;
     Debug("current") << "smt scope: returning to " << s_smtEngine_current << std::endl;
   }
+
+  /**
+   * This returns the StatisticsRegistry attached to the currently in scope
+   * SmtEngine.
+   */
+  static StatisticsRegistry* currentStatisticsRegistry() {
+    Assert(smtEngineInScope());
+    return s_smtEngine_current->d_statisticsRegistry;
+  }
+
 };/* class SmtScope */
 
+
 }/* CVC4::smt namespace */
 }/* CVC4 namespace */