diff options
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
| -rw-r--r-- | src/expr/expr_manager_template.cpp | 4 |
1 files changed, 4 insertions, 0 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); |