1 files changed, 31 insertions, 32 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 2bca01e08..40ed674c0 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -41,40 +41,39 @@
 #include "util/result.h"
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::parser;
-using namespace CVC4::main;
+using namespace CVC5;
+using namespace CVC5::parser;
+using namespace CVC5::main;
 
-namespace CVC4 {
-  namespace main {
-    /** Global options variable */
-    thread_local Options* pOptions;
+namespace CVC5 {
+namespace main {
+/** Global options variable */
+thread_local Options* pOptions;
 
-    /** Full argv[0] */
-    const char *progPath;
+/** Full argv[0] */
+const char* progPath;
 
-    /** Just the basename component of argv[0] */
-    const std::string *progName;
+/** Just the basename component of argv[0] */
+const std::string* progName;
 
-    /** A pointer to the CommandExecutor (the signal handlers need it) */
-    std::unique_ptr<CVC4::main::CommandExecutor> pExecutor;
+/** A pointer to the CommandExecutor (the signal handlers need it) */
+std::unique_ptr<CVC5::main::CommandExecutor> pExecutor;
 
-    /** The time point the binary started, accessible to signal handlers */
-    std::unique_ptr<TotalTimer> totalTime;
+/** The time point the binary started, accessible to signal handlers */
+std::unique_ptr<TotalTimer> totalTime;
 
-    TotalTimer::~TotalTimer()
-    {
-      if (pExecutor != nullptr)
-      {
-        auto duration = std::chrono::steady_clock::now() - d_start;
-        pExecutor->getSmtEngine()->setTotalTimeStatistic(
-            std::chrono::duration<double>(duration).count());
-      }
+TotalTimer::~TotalTimer()
+{
+  if (pExecutor != nullptr)
+  {
+    auto duration = std::chrono::steady_clock::now() - d_start;
+    pExecutor->getSmtEngine()->setTotalTimeStatistic(
+        std::chrono::duration<double>(duration).count());
+  }
     }
 
-  }/* CVC4::main namespace */
-}/* CVC4 namespace */
-
+    }  // namespace main
+    }  // namespace CVC5
 
 void printUsage(Options& opts, bool full) {
   stringstream ss;
@@ -176,12 +175,12 @@ int runCvc4(int argc, char* argv[], Options& opts) {
 
   // Determine which messages to show based on smtcomp_mode and verbosity
   if(Configuration::isMuzzledBuild()) {
-    DebugChannel.setStream(&CVC4::null_os);
-    TraceChannel.setStream(&CVC4::null_os);
-    NoticeChannel.setStream(&CVC4::null_os);
-    ChatChannel.setStream(&CVC4::null_os);
-    MessageChannel.setStream(&CVC4::null_os);
-    WarningChannel.setStream(&CVC4::null_os);
+    DebugChannel.setStream(&CVC5::null_os);
+    TraceChannel.setStream(&CVC5::null_os);
+    NoticeChannel.setStream(&CVC5::null_os);
+    ChatChannel.setStream(&CVC5::null_os);
+    MessageChannel.setStream(&CVC5::null_os);
+    WarningChannel.setStream(&CVC5::null_os);
   }
 
   // important even for muzzled builds (to get result output right)