diff options
Diffstat (limited to 'src/main/command_executor.h')
| -rw-r--r-- | src/main/command_executor.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/main/command_executor.h b/src/main/command_executor.h index cbc71b075..5395cc804 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -28,6 +28,8 @@ namespace CVC4 { namespace main { class CommandExecutor { +private: + std::string d_lastStatistics; protected: ExprManager& d_exprMgr; |