diff options
Diffstat (limited to 'src/main/driver_unified.cpp')
-rw-r--r-- | src/main/driver_unified.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index d2adf97c4..7c2b7b89e 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -318,13 +318,17 @@ int runCvc4(int argc, char* argv[], Options& opts) { *opts[options::replayLog] << flush; } + // make sure out and err streams are flushed too + *opts[options::out] << flush; + *opts[options::err] << flush; + #ifdef CVC4_DEBUG if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) { _exit(returnValue); } #else /* CVC4_DEBUG */ if(opts[options::earlyExit]) { - _exit(returnValue); + _exit(returnValue); } #endif /* CVC4_DEBUG */ } |