diff options
Diffstat (limited to 'src/expr/expr_manager_template.h')
| -rw-r--r-- | src/expr/expr_manager_template.h | 8 |
1 files changed, 7 insertions, 1 deletions
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 */ |