2 files changed, 11 insertions, 1 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 82cabbd3e..cb8ad710f 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -1039,6 +1039,10 @@ SExpr ExprManager::getStatistic(const std::string& name) const throw() {
   return d_nodeManager->getStatisticsRegistry()->getStatistic(name);
 }
 
+void ExprManager::safeFlushStatistics(int fd) const {
+  d_nodeManager->getStatisticsRegistry()->safeFlushInformation(fd);
+}
+
 namespace expr {
 
 Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 9e962d970..07ace173c 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -545,7 +545,7 @@ public:
    * @param type the type for the new bound variable
    */
   Expr mkBoundVar(Type type);
-  
+
   /**
    * Create unique variable of type 
    */
@@ -557,6 +557,12 @@ public:
   /** Get a reference to the statistics registry for this ExprManager */
   SExpr getStatistic(const std::string& name) const throw();
 
+  /**
+   * Flushes statistics for this ExprManager to a file descriptor. Safe to use
+   * in a signal handler.
+   */
+  void safeFlushStatistics(int fd) const;
+
   /** Export an expr to a different ExprManager */
   //static Expr exportExpr(const Expr& e, ExprManager* em);
   /** Export a type to a different ExprManager */