summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGereon Kremer <nafur42@gmail.com>2021-06-04 15:17:57 +0200
committerGitHub <noreply@github.com>2021-06-04 08:17:57 -0500
commit2e001991f926c307ff0f812dafca4d9dc6e4d831 (patch)
tree982fc4e34b308f2f4ba44d0c1cd140c5839b2cbe /src
parentadf497af7a3fc8b06b875eaf9feca2568d0ba9d8 (diff)
Add missing dereference (#6684)
Diffstat (limited to 'src')
-rw-r--r--src/main/driver_unified.cpp2
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback