diff options
Diffstat (limited to 'src/main')
| -rw-r--r-- | src/main/driver_unified.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 79c98924a..4f82ac1ae 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -499,7 +499,7 @@ int runCvc5(int argc, char* argv[], Options& opts) #ifdef CVC5_COMPETITION_MODE if (cvc5::options::getOut(opts) != nullptr) { - cvc5::options::getOut(opts) << std::flush; + *cvc5::options::getOut(opts) << std::flush; } // exit, don't return (don't want destructors to run) // _exit() from unistd.h doesn't run global destructors |