Rename CVC4_ macros to CVC5_. (#6327)

20 files changed, 108 insertions, 108 deletions

diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 0be0b80e1..93ca679f3 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -27,7 +27,7 @@ add_custom_target(units
   COMMAND ctest --output-on-failure -L "unit" -j${CTEST_NTHREADS} $$ARGS
   DEPENDS build-units)
 
-set(CVC4_UNIT_TEST_FLAGS_BLACK
+set(CVC5_UNIT_TEST_FLAGS_BLACK
   -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
   -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)
 
@@ -35,7 +35,7 @@ set(CVC4_UNIT_TEST_FLAGS_BLACK
 macro(cvc4_add_unit_test is_white name output_dir)
   set(test_src ${CMAKE_CURRENT_LIST_DIR}/${name}.cpp)
   add_executable(${name} ${test_src})
-  target_compile_definitions(${name} PRIVATE ${CVC4_UNIT_TEST_FLAGS_BLACK})
+  target_compile_definitions(${name} PRIVATE ${CVC5_UNIT_TEST_FLAGS_BLACK})
   gtest_add_tests(TARGET ${name})
   target_link_libraries(${name} PUBLIC main-test)
   target_link_libraries(${name} PUBLIC GTest::Main)
diff --git a/test/unit/context/cdlist_black.cpp b/test/unit/context/cdlist_black.cpp
index a3241d058..c944b0722 100644
--- a/test/unit/context/cdlist_black.cpp
+++ b/test/unit/context/cdlist_black.cpp
@@ -138,7 +138,7 @@ TEST_F(TestContextBlackCDList, empty_iterator)
 
 TEST_F(TestContextBlackCDList, out_of_memory)
 {
-#ifndef CVC4_MEMORY_LIMITING_DISABLED
+#ifndef CVC5_MEMORY_LIMITING_DISABLED
   CDList<uint32_t> list(d_context.get());
   test::WithLimitedMemory wlm(1);
 
diff --git a/test/unit/context/context_black.cpp b/test/unit/context/context_black.cpp
index 0ad830162..ee5140da3 100644
--- a/test/unit/context/context_black.cpp
+++ b/test/unit/context/context_black.cpp
@@ -91,10 +91,10 @@ TEST_F(TestContextBlack, push_pop)
   // the interface doesn't declare any exceptions
   d_context->push();
   d_context->pop();
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(d_context->pop(), "Cannot pop below level 0");
   ASSERT_DEATH(d_context->pop(), "Cannot pop below level 0");
-#endif /* CVC4_ASSERTIONS */
+#endif /* CVC5_ASSERTIONS */
 }
 
 TEST_F(TestContextBlack, dtor)
diff --git a/test/unit/context/context_mm_black.cpp b/test/unit/context/context_mm_black.cpp
index 0f031ef5b..22b15d70d 100644
--- a/test/unit/context/context_mm_black.cpp
+++ b/test/unit/context/context_mm_black.cpp
@@ -36,7 +36,7 @@ class TestContextBlackMM : public TestInternal
 
 TEST_F(TestContextBlackMM, push_pop)
 {
-#ifdef CVC4_DEBUG_CONTEXT_MEMORY_MANAGER
+#ifdef CVC5_DEBUG_CONTEXT_MEMORY_MANAGER
 #warning "Using the debug context memory manager, omitting unit tests"
 #else
   // Push, then allocate, then pop
diff --git a/test/unit/memory.h b/test/unit/memory.h
index 726404e5e..45c65c202 100644
--- a/test/unit/memory.h
+++ b/test/unit/memory.h
@@ -20,7 +20,7 @@
  **
  ** The WithLimitedMemory destructor will re-establish the previous limit.
  **
- ** This class does not exist in CVC4_MEMORY_LIMITING_DISABLED is defined.
+ ** This class does not exist in CVC5_MEMORY_LIMITING_DISABLED is defined.
  ** This can be disabled for a variety of reasons.
  ** If this is disabled, there will be a function:
  **   void WarnWithLimitedMemoryDisabledReason()
@@ -39,24 +39,24 @@
 #include "base/check.h"
 #include "base/configuration_private.h"
 
-// Conditionally define CVC4_MEMORY_LIMITING_DISABLED.
+// Conditionally define CVC5_MEMORY_LIMITING_DISABLED.
 #ifdef __APPLE__
-#  define CVC4_MEMORY_LIMITING_DISABLED 1
-#  define CVC4_MEMORY_LIMITING_DISABLED_REASON "setrlimit() is broken on Mac."
+#define CVC5_MEMORY_LIMITING_DISABLED 1
+#define CVC5_MEMORY_LIMITING_DISABLED_REASON "setrlimit() is broken on Mac."
 #else /* __APPLE__ */
 
 // Tests cannot expect bad_alloc to be thrown due to limit memory using
 // setrlimit when ASAN is enable. ASAN instead aborts on mmap failures.
 #  if IS_ASAN_BUILD
-#    define CVC4_MEMORY_LIMITING_DISABLED 1
-#    define CVC4_MEMORY_LIMITING_DISABLED_REASON "ASAN's mmap failures abort."
+#define CVC5_MEMORY_LIMITING_DISABLED 1
+#define CVC5_MEMORY_LIMITING_DISABLED_REASON "ASAN's mmap failures abort."
 #  endif
 #endif
 
 namespace cvc5 {
 namespace test {
 
-#ifndef CVC4_MEMORY_LIMITING_DISABLED
+#ifndef CVC5_MEMORY_LIMITING_DISABLED
 class WithLimitedMemory {
  public:
   WithLimitedMemory() { remember(); }
@@ -89,9 +89,9 @@ class WithLimitedMemory {
 }  // namespace test
 }  // namespace cvc5
 
-// Remove CVC4_MEMORY_LIMITING_DISABLED_REASON if it is defined.
-#ifdef CVC4_MEMORY_LIMITING_DISABLED_REASON
-#undef CVC4_MEMORY_LIMITING_DISABLED_REASON
-#endif /* CVC4_MEMORY_LIMITING_DISABLED_REASON */
+// Remove CVC5_MEMORY_LIMITING_DISABLED_REASON if it is defined.
+#ifdef CVC5_MEMORY_LIMITING_DISABLED_REASON
+#undef CVC5_MEMORY_LIMITING_DISABLED_REASON
+#endif /* CVC5_MEMORY_LIMITING_DISABLED_REASON */
 
 #endif /* __CVC5__TEST__MEMORY_H */
diff --git a/test/unit/node/kind_map_black.cpp b/test/unit/node/kind_map_black.cpp
index 7da3e5715..428da7206 100644
--- a/test/unit/node/kind_map_black.cpp
+++ b/test/unit/node/kind_map_black.cpp
@@ -39,7 +39,7 @@ TEST_F(TestNodeBlackKindMap, simple)
   ASSERT_TRUE(map.test(AND));
   map.reset(AND);
   ASSERT_FALSE(map.test(AND));
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_THROW(map.set(LAST_KIND), AssertArgumentException);
 #endif
 }
diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index cfe008ec0..b63541d6c 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -186,7 +186,7 @@ TEST_F(TestNodeBlackNode, operator_not_equals)
 /* operator[] */
 TEST_F(TestNodeBlackNode, operator_square)
 {
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   // Basic bounds check on a node w/out children
   ASSERT_DEATH(Node::null()[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren");
   ASSERT_DEATH(Node::null()[0], "i >= 0 && unsigned\\(i\\) < d_nchildren");
@@ -205,7 +205,7 @@ TEST_F(TestNodeBlackNode, operator_square)
   ASSERT_EQ(tb, ite[1]);
   ASSERT_EQ(eb, ite[2]);
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   // Bounds check on a node with children
   ASSERT_DEATH(ite == ite[-1], "i >= 0 && unsigned\\(i\\) < d_nchildren");
   ASSERT_DEATH(ite == ite[4], "i >= 0 && unsigned\\(i\\) < d_nchildren");
@@ -422,7 +422,7 @@ TEST_F(TestNodeBlackNode, getOperator)
   ASSERT_EQ(a.getNumChildren(), 0);
 
   ASSERT_EQ(f, fa.getOperator());
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(f.getOperator(), "mk == kind::metakind::PARAMETERIZED");
   ASSERT_DEATH(a.getOperator(), "mk == kind::metakind::PARAMETERIZED");
 #endif
@@ -443,7 +443,7 @@ TEST_F(TestNodeBlackNode, getNumChildren)
     testNaryExpForSize(AND, n);
   }
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(testNaryExpForSize(AND, 0),
                "getNumChildren\\(\\) >= "
                "kind::metakind::getMinArityForKind\\(getKind\\(\\)\\)");
@@ -456,7 +456,7 @@ TEST_F(TestNodeBlackNode, getNumChildren)
   ASSERT_DEATH(testNaryExpForSize(NOT, 2),
                "getNumChildren\\(\\) <= "
                "kind::metakind::getMaxArityForKind\\(getKind\\(\\)\\)");
-#endif /* CVC4_ASSERTIONS */
+#endif /* CVC5_ASSERTIONS */
 }
 
 TEST_F(TestNodeBlackNode, iterator)
diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp
index 2b8ef7a04..fbf2b9108 100644
--- a/test/unit/node/node_builder_black.cpp
+++ b/test/unit/node/node_builder_black.cpp
@@ -55,7 +55,7 @@ TEST_F(TestNodeBlackNodeBuilder, ctors)
   /* Default size tests. */
   NodeBuilder def;
   ASSERT_EQ(def.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(def.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
 
@@ -65,7 +65,7 @@ TEST_F(TestNodeBlackNodeBuilder, ctors)
 
   NodeBuilder from_nm(d_nodeManager.get());
   ASSERT_EQ(from_nm.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(from_nm.getNumChildren(),
                "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
@@ -77,7 +77,7 @@ TEST_F(TestNodeBlackNodeBuilder, ctors)
   /* Copy constructors */
   NodeBuilder copy(def);
   ASSERT_EQ(copy.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(copy.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
 }
@@ -100,7 +100,7 @@ TEST_F(TestNodeBlackNodeBuilder, getKind)
   ASSERT_EQ(noKind.getKind(), PLUS);
 
   Node n = noKind;
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(noKind.getKind(), "!isUsed\\(\\)");
 #endif
 
@@ -115,7 +115,7 @@ TEST_F(TestNodeBlackNodeBuilder, getNumChildren)
   Node x(d_skolemManager->mkDummySkolem("x", *d_intTypeNode));
 
   NodeBuilder nb;
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
 
@@ -126,7 +126,7 @@ TEST_F(TestNodeBlackNodeBuilder, getNumChildren)
   ASSERT_EQ(nb.getNumChildren(), 4u);
 
   nb.clear();
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
 
@@ -139,7 +139,7 @@ TEST_F(TestNodeBlackNodeBuilder, getNumChildren)
   nb << x << x << x;
   ASSERT_EQ(nb.getNumChildren(), 6u);
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(nb << PLUS, "getKind\\(\\) == kind::UNDEFINED_KIND");
   Node n = nb;
   ASSERT_DEATH(nb.getNumChildren(), "!isUsed\\(\\)");
@@ -154,7 +154,7 @@ TEST_F(TestNodeBlackNodeBuilder, operator_square)
   Node i_2 = d_nodeManager->mkConst(true);
   Node i_K = d_nodeManager->mkNode(NOT, i_0);
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(arr[-1], "index out of range");
   ASSERT_DEATH(arr[0], "index out of range");
 #endif
@@ -184,7 +184,7 @@ TEST_F(TestNodeBlackNodeBuilder, operator_square)
   }
   ASSERT_EQ(arr[K], i_K);
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   Node n = arr;
   ASSERT_DEATH(arr[0], "!isUsed\\(\\)");
 #endif
@@ -194,7 +194,7 @@ TEST_F(TestNodeBlackNodeBuilder, clear)
 {
   NodeBuilder nb;
   ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
 
@@ -205,7 +205,7 @@ TEST_F(TestNodeBlackNodeBuilder, clear)
 
   nb.clear();
   ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
 
@@ -221,14 +221,14 @@ TEST_F(TestNodeBlackNodeBuilder, clear)
   push_back(nb, K);
   nb.clear();
   ASSERT_EQ(nb.getKind(), UNDEFINED_KIND);
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(nb.getNumChildren(), "getKind\\(\\) != kind::UNDEFINED_KIND");
 #endif
 }
 
 TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind)
 {
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   NodeBuilder spec(d_specKind);
   ASSERT_DEATH(spec << PLUS, "can't redefine the Kind of a NodeBuilder");
 #endif
@@ -246,20 +246,20 @@ TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_kind)
   nb << d_nodeManager->mkConst(true) << d_nodeManager->mkConst(false);
   nb.clear(PLUS);
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   Node n;
   ASSERT_DEATH(n = nb, "Nodes with kind PLUS must have at least 2 children");
   nb.clear(PLUS);
 #endif
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(nb << PLUS, "can't redefine the Kind of a NodeBuilder");
 #endif
 
   NodeBuilder testRef;
   ASSERT_EQ((testRef << d_specKind).getKind(), d_specKind);
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   NodeBuilder testTwo;
   ASSERT_DEATH(testTwo << d_specKind << PLUS,
                "can't redefine the Kind of a NodeBuilder");
@@ -284,7 +284,7 @@ TEST_F(TestNodeBlackNodeBuilder, operator_stream_insertion_node)
   ASSERT_EQ(nb.getKind(), d_specKind);
   ASSERT_EQ(nb.getNumChildren(), K);
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   Node n = nb;
   ASSERT_DEATH(nb << n, "!isUsed\\(\\)");
 #endif
@@ -317,7 +317,7 @@ TEST_F(TestNodeBlackNodeBuilder, append)
       d_nodeManager->mkNode(PLUS, r, d_nodeManager->mkNode(UMINUS, s), t));
   Node q = d_nodeManager->mkNode(AND, x, z, d_nodeManager->mkNode(NOT, y));
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(d_nodeManager->mkNode(XOR, y, x, x),
                "Nodes with kind XOR must have at most 2 children");
 #endif
@@ -380,7 +380,7 @@ TEST_F(TestNodeBlackNodeBuilder, operator_node_cast)
   ASSERT_EQ(nexplicit.getKind(), d_specKind);
   ASSERT_EQ(nexplicit.getNumChildren(), K);
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(Node blah = implicit, "!isUsed\\(\\)");
 #endif
 }
diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp
index 6ad6f583c..a2d25c8d8 100644
--- a/test/unit/node/node_manager_black.cpp
+++ b/test/unit/node/node_manager_black.cpp
@@ -302,7 +302,7 @@ TEST_F(TestNodeBlackNodeManager, mkPredicateType)
 /* This test is only valid if assertions are enabled. */
 TEST_F(TestNodeBlackNodeManager, mkNode_too_few_children)
 {
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   Node x = d_skolemManager->mkDummySkolem("x", d_nodeManager->booleanType());
   ASSERT_DEATH(d_nodeManager->mkNode(AND, x),
                "Nodes with kind AND must have at least 2 children");
@@ -312,7 +312,7 @@ TEST_F(TestNodeBlackNodeManager, mkNode_too_few_children)
 /* This test is only valid if assertions are enabled. */
 TEST_F(TestNodeBlackNodeManager, mkNode_too_many_children)
 {
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   std::vector<Node> vars;
   const uint32_t max = metakind::getMaxArityForKind(AND);
   TypeNode boolType = d_nodeManager->booleanType();
diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp
index a13e76d03..986eac870 100644
--- a/test/unit/node/node_manager_white.cpp
+++ b/test/unit/node/node_manager_white.cpp
@@ -46,9 +46,9 @@ TEST_F(TestNodeWhiteNodeManager, oversized_node_builder)
   ASSERT_NO_THROW(nb.realloc(15));
   ASSERT_NO_THROW(nb.realloc(25));
   ASSERT_NO_THROW(nb.realloc(256));
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(nb.realloc(100), "toSize > d_nvMaxChildren");
-#endif /* CVC4_ASSERTIONS */
+#endif /* CVC5_ASSERTIONS */
   ASSERT_NO_THROW(nb.realloc(257));
   ASSERT_NO_THROW(nb.realloc(4000));
   ASSERT_NO_THROW(nb.realloc(20000));
@@ -56,9 +56,9 @@ TEST_F(TestNodeWhiteNodeManager, oversized_node_builder)
   ASSERT_NO_THROW(nb.realloc(65535));
   ASSERT_NO_THROW(nb.realloc(65536));
   ASSERT_NO_THROW(nb.realloc(67108863));
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(nb.realloc(67108863), "toSize > d_nvMaxChildren");
-#endif /* CVC4_ASSERTIONS */
+#endif /* CVC5_ASSERTIONS */
 }
 
 TEST_F(TestNodeWhiteNodeManager, topological_sort)
diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp
index 5b695030e..27d008228 100644
--- a/test/unit/parser/parser_black.cpp
+++ b/test/unit/parser/parser_black.cpp
@@ -238,7 +238,7 @@ TEST_F(TestParserBlackCvCParser, good_inputs)
 TEST_F(TestParserBlackCvCParser, bad_inputs)
 {
 // competition builds don't do any checking
-#ifndef CVC4_COMPETITION_MODE
+#ifndef CVC5_COMPETITION_MODE
   tryBadInput("ASSERT;");  // no args
   tryBadInput("QUERY");
   tryBadInput("CHECKSAT");
@@ -278,7 +278,7 @@ TEST_F(TestParserBlackCvCParser, good_exprs)
 TEST_F(TestParserBlackCvCParser, bad_exprs)
 {
 // competition builds don't do any checking
-#ifndef CVC4_COMPETITION_MODE
+#ifndef CVC5_COMPETITION_MODE
   tryBadInput("a AND");             // wrong arity
   tryBadInput("AND(a,b)");          // not infix
   tryBadInput("(OR (AND a b) c)");  // not infix
@@ -326,7 +326,7 @@ TEST_F(TestParserBlackSmt2Parser, good_inputs)
 TEST_F(TestParserBlackSmt2Parser, bad_inputs)
 {
   // competition builds don't do any checking
-#ifndef CVC4_COMPETITION_MODE
+#ifndef CVC5_COMPETITION_MODE
   // no arguments
   tryBadInput("(assert)");
   // illegal character in symbol
@@ -366,7 +366,7 @@ TEST_F(TestParserBlackSmt2Parser, good_exprs)
 TEST_F(TestParserBlackSmt2Parser, bad_exprs)
 {
 // competition builds don't do any checking
-#ifndef CVC4_COMPETITION_MODE
+#ifndef CVC5_COMPETITION_MODE
   tryBadExpr("(and)");                     // wrong arity
   tryBadExpr("(and a b");                  // no closing paren
   tryBadExpr("(a and b)");                 // infix
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index b898e1344..fc5484a1f 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -21,7 +21,7 @@ cvc4_add_unit_test_white(check_white util)
 cvc4_add_unit_test_black(configuration_black util)
 cvc4_add_unit_test_black(datatype_black util)
 cvc4_add_unit_test_black(exception_black util)
-if(CVC4_USE_SYMFPU)
+if(CVC5_USE_SYMFPU)
 cvc4_add_unit_test_black(floatingpoint_black util)
 endif()
 cvc4_add_unit_test_black(integer_black util)
@@ -29,7 +29,7 @@ cvc4_add_unit_test_white(integer_white util)
 cvc4_add_unit_test_black(output_black util)
 cvc4_add_unit_test_black(rational_black util)
 cvc4_add_unit_test_white(rational_white util)
-if(CVC4_USE_POLY_IMP)
+if(CVC5_USE_POLY_IMP)
 cvc4_add_unit_test_black(real_algebraic_number_black util)
 endif()
 cvc4_add_unit_test_black(stats_black util)
diff --git a/test/unit/util/assert_white.cpp b/test/unit/util/assert_white.cpp
index bab612b62..245ef8aaa 100644
--- a/test/unit/util/assert_white.cpp
+++ b/test/unit/util/assert_white.cpp
@@ -29,7 +29,7 @@ class TestUtilWhite : public TestInternal
 
 TEST_F(TestUtilWhite, Assert)
 {
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(Assert(false), "false");
 #else
   ASSERT_NO_THROW(Assert(false));
@@ -41,7 +41,7 @@ TEST_F(TestUtilWhite, Assert)
 
 TEST_F(TestUtilWhite, AssertArgument)
 {
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_THROW(AssertArgument(false, "x"), AssertArgumentException);
 #else
   ASSERT_NO_THROW(AssertArgument(false, "x"));
diff --git a/test/unit/util/binary_heap_black.cpp b/test/unit/util/binary_heap_black.cpp
index c00aeaeb2..76462b687 100644
--- a/test/unit/util/binary_heap_black.cpp
+++ b/test/unit/util/binary_heap_black.cpp
@@ -60,7 +60,7 @@ TEST_F(TestUtilBlackBinaryHeap, heap_series)
   // First test a heap of 1 element
   ASSERT_EQ(heap.size(), 0u);
   ASSERT_TRUE(heap.empty());
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(heap.top(), "!empty\\(\\)");
   ASSERT_DEATH(heap.pop(), "!empty\\(\\)");
 #endif
@@ -77,7 +77,7 @@ TEST_F(TestUtilBlackBinaryHeap, heap_series)
   ASSERT_NO_THROW(heap.erase(h5));
   ASSERT_TRUE(heap.empty());
   ASSERT_EQ(heap.size(), 0u);
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(heap.top(), "!empty\\(\\)");
   ASSERT_DEATH(heap.pop(), "!empty\\(\\)");
 #endif
@@ -135,7 +135,7 @@ TEST_F(TestUtilBlackBinaryHeap, heap_series)
   ASSERT_TRUE(heap.begin() == heap.end());
   ASSERT_TRUE(heap.empty());
   ASSERT_EQ(heap.size(), 0u);
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   ASSERT_DEATH(heap.top(), "!empty\\(\\)");
   ASSERT_DEATH(heap.pop(), "!empty\\(\\)");
 #endif
diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp
index 2e266ce58..1ec9c923c 100644
--- a/test/unit/util/boolean_simplification_black.cpp
+++ b/test/unit/util/boolean_simplification_black.cpp
@@ -124,7 +124,7 @@ TEST_F(TestUtilBlackBooleanSimplification, negate)
   out = d_fa.andNode(d_ac).notNode();
   test_nodes_equal(out, BooleanSimplification::negate(in));
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   in = Node();
   ASSERT_THROW(BooleanSimplification::negate(in), AssertArgumentException);
 #endif
@@ -166,7 +166,7 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyClause)
                               << d_hfc << d_ac << d_d.andNode(d_b);
   test_nodes_equal(out, BooleanSimplification::simplifyClause(in));
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   in = d_nodeManager->mkNode(kind::AND, d_a, d_b);
   ASSERT_THROW(BooleanSimplification::simplifyClause(in),
                AssertArgumentException);
@@ -212,7 +212,7 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyHornClause)
         << d_hfc << d_ac << d_d.notNode();
   test_nodes_equal(out, BooleanSimplification::simplifyHornClause(in));
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   in = d_nodeManager->mkNode(kind::OR, d_a, d_b);
   ASSERT_THROW(BooleanSimplification::simplifyHornClause(in),
                AssertArgumentException);
@@ -241,7 +241,7 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyConflict)
                                << d_hfc.orNode(d_ac) << d_d << d_b;
   test_nodes_equal(out, BooleanSimplification::simplifyConflict(in));
 
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
   in = d_nodeManager->mkNode(kind::OR, d_a, d_b);
   ASSERT_THROW(BooleanSimplification::simplifyConflict(in),
                AssertArgumentException);
diff --git a/test/unit/util/check_white.cpp b/test/unit/util/check_white.cpp
index 4909e3a58..d517e4364 100644
--- a/test/unit/util/check_white.cpp
+++ b/test/unit/util/check_white.cpp
@@ -31,7 +31,7 @@ class TestUtilWhiteCheck : public TestInternal
   // This test just checks that this statement compiles.
   std::string terminalCvc4Fatal() const
   {
-    CVC4_FATAL() << "This is a test that confirms that CVC4_FATAL can be a "
+    CVC5_FATAL() << "This is a test that confirms that CVC5_FATAL can be a "
                     "terminal statement in a function that has a non-void "
                     "return type.";
   }
@@ -45,8 +45,8 @@ TEST_F(TestUtilWhiteCheck, check)
 TEST_F(TestUtilWhiteCheck, dcheck)
 {
   Assert(K_ONE == 1) << "always passes";
-#ifndef CVC4_ASSERTIONS
-  Assert(false) << "Will not be compiled in when CVC4_ASSERTIONS off.";
+#ifndef CVC5_ASSERTIONS
+  Assert(false) << "Will not be compiled in when CVC5_ASSERTIONS off.";
 #endif
 }
 
diff --git a/test/unit/util/configuration_black.cpp b/test/unit/util/configuration_black.cpp
index 35bfd4d78..508aa179b 100644
--- a/test/unit/util/configuration_black.cpp
+++ b/test/unit/util/configuration_black.cpp
@@ -27,46 +27,46 @@ class TestUtilBlackConfiguration : public TestInternal
 TEST_F(TestUtilBlackConfiguration, static_flags)
 {
   const bool debug =
-#ifdef CVC4_DEBUG
+#ifdef CVC5_DEBUG
       true;
-#else  /* CVC4_DEBUG */
+#else  /* CVC5_DEBUG */
       false;
-#endif /* CVC4_DEBUG */
+#endif /* CVC5_DEBUG */
 
   const bool tracing =
-#ifdef CVC4_TRACING
+#ifdef CVC5_TRACING
       true;
-#else  /* CVC4_TRACING */
+#else  /* CVC5_TRACING */
       false;
-#endif /* CVC4_TRACING */
+#endif /* CVC5_TRACING */
 
   const bool muzzled =
-#ifdef CVC4_MUZZLE
+#ifdef CVC5_MUZZLE
       true;
-#else  /* CVC4_MUZZLE */
+#else  /* CVC5_MUZZLE */
       false;
-#endif /* CVC4_MUZZLE */
+#endif /* CVC5_MUZZLE */
 
   const bool assertions =
-#ifdef CVC4_ASSERTIONS
+#ifdef CVC5_ASSERTIONS
       true;
-#else  /* CVC4_ASSERTIONS */
+#else  /* CVC5_ASSERTIONS */
       false;
-#endif /* CVC4_ASSERTIONS */
+#endif /* CVC5_ASSERTIONS */
 
   const bool coverage =
-#ifdef CVC4_COVERAGE
+#ifdef CVC5_COVERAGE
       true;
-#else  /* CVC4_COVERAGE */
+#else  /* CVC5_COVERAGE */
       false;
-#endif /* CVC4_COVERAGE */
+#endif /* CVC5_COVERAGE */
 
   const bool profiling =
-#ifdef CVC4_PROFILING
+#ifdef CVC5_PROFILING
       true;
-#else  /* CVC4_PROFILING */
+#else  /* CVC5_PROFILING */
       false;
-#endif /* CVC4_PROFILING */
+#endif /* CVC5_PROFILING */
 
   ASSERT_EQ(Configuration::isDebugBuild(), debug);
   ASSERT_EQ(Configuration::isTracingBuild(), tracing);
diff --git a/test/unit/util/output_black.cpp b/test/unit/util/output_black.cpp
index e951dd114..09991a6d0 100644
--- a/test/unit/util/output_black.cpp
+++ b/test/unit/util/output_black.cpp
@@ -82,7 +82,7 @@ TEST_F(TestUtilBlackOutput, output)
   Trace.on("foo");
   Trace("foo") << "tracing3";
 
-#ifdef CVC4_MUZZLE
+#ifdef CVC5_MUZZLE
 
   ASSERT_EQ(d_debugStream.str(), "");
   ASSERT_EQ(d_messageStream.str(), "");
@@ -91,32 +91,32 @@ TEST_F(TestUtilBlackOutput, output)
   ASSERT_EQ(d_noticeStream.str(), "");
   ASSERT_EQ(d_traceStream.str(), "");
 
-#else /* CVC4_MUZZLE */
+#else /* CVC5_MUZZLE */
 
-#ifdef CVC4_DEBUG
+#ifdef CVC5_DEBUG
   ASSERT_EQ(d_debugStream.str(), "testing1testing3");
-#else  /* CVC4_DEBUG */
+#else  /* CVC5_DEBUG */
   ASSERT_EQ(d_debugStream.str(), "");
-#endif /* CVC4_DEBUG */
+#endif /* CVC5_DEBUG */
 
   ASSERT_EQ(d_messageStream.str(), "a message");
   ASSERT_EQ(d_warningStream.str(), "bad warning!");
   ASSERT_EQ(d_chatStream.str(), "chatty");
   ASSERT_EQ(d_noticeStream.str(), "note");
 
-#ifdef CVC4_TRACING
+#ifdef CVC5_TRACING
   ASSERT_EQ(d_traceStream.str(), "tracing1tracing3");
-#else  /* CVC4_TRACING */
+#else  /* CVC5_TRACING */
   ASSERT_EQ(d_traceStream.str(), "");
-#endif /* CVC4_TRACING */
+#endif /* CVC5_TRACING */
 
-#endif /* CVC4_MUZZLE */
+#endif /* CVC5_MUZZLE */
 }
 
 TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be)
 {
   Debug.on("foo");
-#ifndef CVC4_DEBUG
+#ifndef CVC5_DEBUG
   ASSERT_FALSE(Debug.isOn("foo"));
   Debug("foo") << failure() << std::endl;
 #else
@@ -125,7 +125,7 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be)
   Debug.off("foo");
 
   Trace.on("foo");
-#ifndef CVC4_TRACING
+#ifndef CVC5_TRACING
   ASSERT_FALSE(Trace.isOn("foo"));
   Trace("foo") << failure() << std::endl;
 #else
@@ -133,7 +133,7 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be)
 #endif
   Trace.off("foo");
 
-#ifdef CVC4_MUZZLE
+#ifdef CVC5_MUZZLE
   ASSERT_FALSE(Debug.isOn("foo"));
   ASSERT_FALSE(Trace.isOn("foo"));
   ASSERT_FALSE(Warning.isOn());
@@ -158,7 +158,7 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be)
 
 TEST_F(TestUtilBlackOutput, simple_print)
 {
-#ifdef CVC4_MUZZLE
+#ifdef CVC5_MUZZLE
 
   Debug.off("yo");
   Debug("yo") << "foobar";
@@ -194,7 +194,7 @@ TEST_F(TestUtilBlackOutput, simple_print)
   ASSERT_EQ(d_noticeStream.str(), std::string());
   d_noticeStream.str("");
 
-#else /* CVC4_MUZZLE */
+#else /* CVC5_MUZZLE */
 
   Debug.off("yo");
   Debug("yo") << "foobar";
@@ -202,11 +202,11 @@ TEST_F(TestUtilBlackOutput, simple_print)
   d_debugStream.str("");
   Debug.on("yo");
   Debug("yo") << "baz foo";
-#ifdef CVC4_DEBUG
+#ifdef CVC5_DEBUG
   ASSERT_EQ(d_debugStream.str(), std::string("baz foo"));
-#else  /* CVC4_DEBUG */
+#else  /* CVC5_DEBUG */
   ASSERT_EQ(d_debugStream.str(), std::string());
-#endif /* CVC4_DEBUG */
+#endif /* CVC5_DEBUG */
   d_debugStream.str("");
 
   Trace.off("yo");
@@ -215,11 +215,11 @@ TEST_F(TestUtilBlackOutput, simple_print)
   d_traceStream.str("");
   Trace.on("yo");
   Trace("yo") << "baz foo";
-#ifdef CVC4_TRACING
+#ifdef CVC5_TRACING
   ASSERT_EQ(d_traceStream.str(), std::string("baz foo"));
-#else  /* CVC4_TRACING */
+#else  /* CVC5_TRACING */
   ASSERT_EQ(d_traceStream.str(), std::string());
-#endif /* CVC4_TRACING */
+#endif /* CVC5_TRACING */
   d_traceStream.str("");
 
   Warning() << "baz foo";
@@ -238,7 +238,7 @@ TEST_F(TestUtilBlackOutput, simple_print)
   ASSERT_EQ(d_noticeStream.str(), std::string("baz foo"));
   d_noticeStream.str("");
 
-#endif /* CVC4_MUZZLE */
+#endif /* CVC5_MUZZLE */
 }
 }  // namespace test
 }  // namespace cvc5
diff --git a/test/unit/util/real_algebraic_number_black.cpp b/test/unit/util/real_algebraic_number_black.cpp
index 507be5ea0..c130023ca 100644
--- a/test/unit/util/real_algebraic_number_black.cpp
+++ b/test/unit/util/real_algebraic_number_black.cpp
@@ -20,8 +20,8 @@
 namespace cvc5 {
 namespace test {
 
-#ifndef CVC4_POLY_IMP
-#error "This unit test should only be enabled for CVC4_POLY_IMP"
+#ifndef CVC5_POLY_IMP
+#error "This unit test should only be enabled for CVC5_POLY_IMP"
 #endif
 
 class TestUtilBlackRealAlgebraicNumber : public TestInternal
diff --git a/test/unit/util/stats_black.cpp b/test/unit/util/stats_black.cpp
index 2ee64ab33..c15b0cd47 100644
--- a/test/unit/util/stats_black.cpp
+++ b/test/unit/util/stats_black.cpp
@@ -36,7 +36,7 @@ class TestUtilBlackStats : public TestInternal
 
 TEST_F(TestUtilBlackStats, stats)
 {
-#ifdef CVC4_STATISTICS_ON
+#ifdef CVC5_STATISTICS_ON
   std::string empty, bar = "bar", baz = "baz";
   ReferenceStat<std::string> refStr("stat #1", empty);
   ReferenceStat<std::string> refStr2("refStr2", bar);