Add missing dereference (#6684)
authorGereon Kremer <nafur42@gmail.com>
Fri, 4 Jun 2021 13:17:57 +0000 (15:17 +0200)
committerGitHub <noreply@github.com>
Fri, 4 Jun 2021 13:17:57 +0000 (08:17 -0500)
src/main/driver_unified.cpp

index 79c98924af98d4831e9aeb068db78cb996cd8855..4f82ac1aefc242cb33d885546cad91a7eb7608e8 100644 (file)
@@ -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