4 files changed, 19 insertions, 19 deletions
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 4dc8880b1..9fbcf7158 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -92,7 +92,7 @@ g_getopt_long_start = 256
 
 ### Source code templates
 
-TPL_HOLDER_MACRO_NAME = 'CVC4_OPTIONS__{id}__FOR_OPTION_HOLDER'
+TPL_HOLDER_MACRO_NAME = 'CVC5_OPTIONS__{id}__FOR_OPTION_HOLDER'
 
 TPL_RUN_HANDLER = \
 """template <> options::{name}__option_t::type runHandlerAndPredicates(
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index ccffd17ec..2dcf26a95 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -95,24 +95,24 @@ void OptionsHandler::checkInstWhenMode(std::string option, InstWhenMode mode)
 // theory/bv/options_handlers.h
 void OptionsHandler::abcEnabledBuild(std::string option, bool value)
 {
-#ifndef CVC4_USE_ABC
+#ifndef CVC5_USE_ABC
   if(value) {
     std::stringstream ss;
     ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
     throw OptionException(ss.str());
   }
-#endif /* CVC4_USE_ABC */
+#endif /* CVC5_USE_ABC */
 }
 
 void OptionsHandler::abcEnabledBuild(std::string option, std::string value)
 {
-#ifndef CVC4_USE_ABC
+#ifndef CVC5_USE_ABC
   if(!value.empty()) {
     std::stringstream ss;
     ss << "option `" << option << "' requires an abc-enabled build of CVC4; this binary was not built with abc support";
     throw OptionException(ss.str());
   }
-#endif /* CVC4_USE_ABC */
+#endif /* CVC5_USE_ABC */
 }
 
 void OptionsHandler::checkBvSatSolver(std::string option, SatSolverMode m)
@@ -255,13 +255,13 @@ void OptionsHandler::setProduceAssertions(std::string option, bool value)
 
 void OptionsHandler::statsEnabledBuild(std::string option, bool value)
 {
-#ifndef CVC4_STATISTICS_ON
+#ifndef CVC5_STATISTICS_ON
   if(value) {
     std::stringstream ss;
     ss << "option `" << option << "' requires a statistics-enabled build of CVC4; this binary was not built with statistics support";
     throw OptionException(ss.str());
   }
-#endif /* CVC4_STATISTICS_ON */
+#endif /* CVC5_STATISTICS_ON */
 }
 
 void OptionsHandler::threadN(std::string option) {
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index 7d1b1802a..9b1271c8b 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -124,8 +124,8 @@ public:
 template<class T>
 void OptionsHandler::checkSatSolverEnabled(std::string option, T m)
 {
-#if !defined(CVC4_USE_CRYPTOMINISAT) && !defined(CVC4_USE_CADICAL) \
-    && !defined(CVC4_USE_KISSAT)
+#if !defined(CVC5_USE_CRYPTOMINISAT) && !defined(CVC5_USE_CADICAL) \
+    && !defined(CVC5_USE_KISSAT)
   std::stringstream ss;
   ss << "option `" << option
      << "' requires CVC4 to be built with CryptoMiniSat or CaDiCaL or Kissat";
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index f158f29e6..520cc491c 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -16,11 +16,11 @@
 
 #if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__)
 // force use of optreset; mingw32 croaks on argv-switching otherwise
-#  include "cvc4autoconfig.h"
-#  define _BSD_SOURCE
-#  undef HAVE_DECL_OPTRESET
-#  define HAVE_DECL_OPTRESET 1
-#  define CVC4_IS_NOT_REALLY_BSD
+#include "cvc4autoconfig.h"
+#define _BSD_SOURCE
+#undef HAVE_DECL_OPTRESET
+#define HAVE_DECL_OPTRESET 1
+#define CVC5_IS_NOT_REALLY_BSD
 #endif /* !_BSD_SOURCE && __MINGW32__ && !__MINGW64__ */
 
 #ifdef __MINGW64__
@@ -30,9 +30,9 @@ extern int optreset;
 #include <getopt.h>
 
 // clean up
-#ifdef CVC4_IS_NOT_REALLY_BSD
+#ifdef CVC5_IS_NOT_REALLY_BSD
 #  undef _BSD_SOURCE
-#endif /* CVC4_IS_NOT_REALLY_BSD */
+#endif /* CVC5_IS_NOT_REALLY_BSD */
 
 #include <unistd.h>
 #include <string.h>
@@ -252,11 +252,11 @@ void Options::setListener(OptionsListener* ol) { d_olisten = ol; }
 
 ${custom_handlers}$
 
-#if defined(CVC4_MUZZLED) || defined(CVC4_COMPETITION_MODE)
+#if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE)
 #  define DO_SEMANTIC_CHECKS_BY_DEFAULT false
-#else /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
+#else /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
 #  define DO_SEMANTIC_CHECKS_BY_DEFAULT true
-#endif /* CVC4_MUZZLED || CVC4_COMPETITION_MODE */
+#endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */
 
 options::OptionsHolder::OptionsHolder() :
   ${module_defaults}$