From: Gereon Kremer <nafur42@gmail.com>
Date: Wed, 2 Jun 2021 16:01:08 +0000 (+0200)
Subject: Use proper variable name (#6670)
X-Git-Tag: cvc5-1.0.0~1656
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e1d476724171293d324ea9f144d1171d9b36b571;p=cvc5.git

Use proper variable name (#6670)

This PR fixes the driver which used an incorrect variable name in competition mode.
---

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 5785505d0..79c98924a 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -497,9 +497,9 @@ int runCvc5(int argc, char* argv[], Options& opts)
     }
 
 #ifdef CVC5_COMPETITION_MODE
-    if (cvc5::options::getOut(options) != nullptr)
+    if (cvc5::options::getOut(opts) != nullptr)
     {
-      cvc5::options::getOut(options) << 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