diff options
Diffstat (limited to 'src/main/command_executor_portfolio.cpp')
| -rw-r--r-- | src/main/command_executor_portfolio.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 9de3b2134..1cc024117 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -330,6 +330,12 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) *d_options[options::out] << d_ostringstreams[portfolioReturn.first]->str(); + // FIXME! MASSIVE HACK!! + if(d_options[options::statistics]) { + pExecutor->flushStatistics(*d_options[options::err]); + } + + exit(0); } /* cleanup this check sat specific stuff */ |