Rename namespace CVC5 to cvc5. (#6258)

87 files changed, 422 insertions, 422 deletions

diff --git a/test/unit/api/datatype_api_black.cpp b/test/unit/api/datatype_api_black.cpp
index 97db622c6..190816921 100644
--- a/test/unit/api/datatype_api_black.cpp
+++ b/test/unit/api/datatype_api_black.cpp
@@ -16,7 +16,7 @@
 
 #include "test_api.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace api;
 
@@ -547,4 +547,4 @@ TEST_F(TestApiBlackDatatype, datatypeSpecializedCons)
   ASSERT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/grammar_black.cpp
index 96ad29503..9c1f750b8 100644
--- a/test/unit/api/grammar_black.cpp
+++ b/test/unit/api/grammar_black.cpp
@@ -16,7 +16,7 @@
 
 #include "test_api.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace api;
 
@@ -122,4 +122,4 @@ TEST_F(TestApiBlackGrammar, addAnyVariable)
   ASSERT_THROW(g1.addAnyVariable(start), CVC4ApiException);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/api/op_black.cpp b/test/unit/api/op_black.cpp
index 2333e5719..0e6626ec5 100644
--- a/test/unit/api/op_black.cpp
+++ b/test/unit/api/op_black.cpp
@@ -14,7 +14,7 @@
 
 #include "test_api.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace api;
 
@@ -178,4 +178,4 @@ TEST_F(TestApiBlackOp, opScopingToString)
   ASSERT_EQ(bitvector_repeat_ot.toString(), op_repr);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/api/op_white.cpp b/test/unit/api/op_white.cpp
index 49a964e9e..909aafcbb 100644
--- a/test/unit/api/op_white.cpp
+++ b/test/unit/api/op_white.cpp
@@ -14,7 +14,7 @@
 
 #include "test_api.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace api;
 
@@ -32,4 +32,4 @@ TEST_F(TestApiWhiteOp, opFromKind)
   ASSERT_EQ(plus, d_solver.mkOp(PLUS));
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp
index f27b30431..ac4542c59 100644
--- a/test/unit/api/result_black.cpp
+++ b/test/unit/api/result_black.cpp
@@ -14,7 +14,7 @@
 
 #include "test_api.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace api;
 
@@ -26,7 +26,7 @@ class TestApiBlackResult : public TestApi
 
 TEST_F(TestApiBlackResult, isNull)
 {
-  CVC5::api::Result res_null;
+  cvc5::api::Result res_null;
   ASSERT_TRUE(res_null.isNull());
   ASSERT_FALSE(res_null.isSat());
   ASSERT_FALSE(res_null.isUnsat());
@@ -37,7 +37,7 @@ TEST_F(TestApiBlackResult, isNull)
   Sort u_sort = d_solver.mkUninterpretedSort("u");
   Term x = d_solver.mkVar(u_sort, "x");
   d_solver.assertFormula(x.eqTerm(x));
-  CVC5::api::Result res = d_solver.checkSat();
+  cvc5::api::Result res = d_solver.checkSat();
   ASSERT_FALSE(res.isNull());
 }
 
@@ -46,9 +46,9 @@ TEST_F(TestApiBlackResult, eq)
   Sort u_sort = d_solver.mkUninterpretedSort("u");
   Term x = d_solver.mkVar(u_sort, "x");
   d_solver.assertFormula(x.eqTerm(x));
-  CVC5::api::Result res;
-  CVC5::api::Result res2 = d_solver.checkSat();
-  CVC5::api::Result res3 = d_solver.checkSat();
+  cvc5::api::Result res;
+  cvc5::api::Result res2 = d_solver.checkSat();
+  cvc5::api::Result res3 = d_solver.checkSat();
   res = res2;
   ASSERT_EQ(res, res2);
   ASSERT_EQ(res3, res2);
@@ -59,7 +59,7 @@ TEST_F(TestApiBlackResult, isSat)
   Sort u_sort = d_solver.mkUninterpretedSort("u");
   Term x = d_solver.mkVar(u_sort, "x");
   d_solver.assertFormula(x.eqTerm(x));
-  CVC5::api::Result res = d_solver.checkSat();
+  cvc5::api::Result res = d_solver.checkSat();
   ASSERT_TRUE(res.isSat());
   ASSERT_FALSE(res.isSatUnknown());
 }
@@ -69,7 +69,7 @@ TEST_F(TestApiBlackResult, isUnsat)
   Sort u_sort = d_solver.mkUninterpretedSort("u");
   Term x = d_solver.mkVar(u_sort, "x");
   d_solver.assertFormula(x.eqTerm(x).notTerm());
-  CVC5::api::Result res = d_solver.checkSat();
+  cvc5::api::Result res = d_solver.checkSat();
   ASSERT_TRUE(res.isUnsat());
   ASSERT_FALSE(res.isSatUnknown());
 }
@@ -82,7 +82,7 @@ TEST_F(TestApiBlackResult, isSatUnknown)
   Sort int_sort = d_solver.getIntegerSort();
   Term x = d_solver.mkVar(int_sort, "x");
   d_solver.assertFormula(x.eqTerm(x).notTerm());
-  CVC5::api::Result res = d_solver.checkSat();
+  cvc5::api::Result res = d_solver.checkSat();
   ASSERT_FALSE(res.isSat());
   ASSERT_TRUE(res.isSatUnknown());
 }
@@ -96,10 +96,10 @@ TEST_F(TestApiBlackResult, isEntailed)
   Term a = x.eqTerm(y).notTerm();
   Term b = x.eqTerm(y);
   d_solver.assertFormula(a);
-  CVC5::api::Result entailed = d_solver.checkEntailed(a);
+  cvc5::api::Result entailed = d_solver.checkEntailed(a);
   ASSERT_TRUE(entailed.isEntailed());
   ASSERT_FALSE(entailed.isEntailmentUnknown());
-  CVC5::api::Result not_entailed = d_solver.checkEntailed(b);
+  cvc5::api::Result not_entailed = d_solver.checkEntailed(b);
   ASSERT_TRUE(not_entailed.isNotEntailed());
   ASSERT_FALSE(not_entailed.isEntailmentUnknown());
 }
@@ -112,10 +112,10 @@ TEST_F(TestApiBlackResult, isEntailmentUnknown)
   Sort int_sort = d_solver.getIntegerSort();
   Term x = d_solver.mkVar(int_sort, "x");
   d_solver.assertFormula(x.eqTerm(x).notTerm());
-  CVC5::api::Result res = d_solver.checkEntailed(x.eqTerm(x));
+  cvc5::api::Result res = d_solver.checkEntailed(x.eqTerm(x));
   ASSERT_FALSE(res.isEntailed());
   ASSERT_TRUE(res.isEntailmentUnknown());
   ASSERT_EQ(res.getUnknownExplanation(), api::Result::UNKNOWN_REASON);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 8f15e9017..fef06fa88 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -16,7 +16,7 @@
 
 #include "test_api.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace api;
 
@@ -1422,7 +1422,7 @@ TEST_F(TestApiBlackSolver, getUnsatCore3)
   {
     d_solver.assertFormula(t);
   }
-  CVC5::api::Result res = d_solver.checkSat();
+  cvc5::api::Result res = d_solver.checkSat();
   ASSERT_TRUE(res.isUnsat());
 }
 
@@ -1533,7 +1533,7 @@ void checkSimpleSeparationConstraints(Solver* solver)
   solver->declareSeparationHeap(integer, integer);
   Term x = solver->mkConst(integer, "x");
   Term p = solver->mkConst(integer, "p");
-  Term heap = solver->mkTerm(CVC5::api::Kind::SEP_PTO, p, x);
+  Term heap = solver->mkTerm(cvc5::api::Kind::SEP_PTO, p, x);
   solver->assertFormula(heap);
   Term nil = solver->mkSepNil(integer);
   solver->assertFormula(nil.eqTerm(solver->mkReal(5)));
@@ -2343,4 +2343,4 @@ TEST_F(TestApiBlackSolver, tupleProject)
 }
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/api/solver_white.cpp b/test/unit/api/solver_white.cpp
index 66a6c70f1..25878f22d 100644
--- a/test/unit/api/solver_white.cpp
+++ b/test/unit/api/solver_white.cpp
@@ -17,7 +17,7 @@
 #include "base/configuration.h"
 #include "test_api.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace api;
 
@@ -54,4 +54,4 @@ TEST_F(TestApiWhiteSolver, getOp)
 }
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/api/sort_black.cpp b/test/unit/api/sort_black.cpp
index f1ec0985a..e0507e749 100644
--- a/test/unit/api/sort_black.cpp
+++ b/test/unit/api/sort_black.cpp
@@ -16,7 +16,7 @@
 
 #include "test_api.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace api;
 
@@ -603,4 +603,4 @@ TEST_F(TestApiBlackSort, sortScopedToString)
 }
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
index 7ac1a881e..117b15394 100644
--- a/test/unit/api/term_black.cpp
+++ b/test/unit/api/term_black.cpp
@@ -14,7 +14,7 @@
 
 #include "test_api.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace api;
 
@@ -848,4 +848,4 @@ TEST_F(TestApiBlackTerm, termScopedToString)
   ASSERT_EQ(x.toString(), "x");
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/api/term_white.cpp b/test/unit/api/term_white.cpp
index de8e94227..e7b7a9cd6 100644
--- a/test/unit/api/term_white.cpp
+++ b/test/unit/api/term_white.cpp
@@ -14,7 +14,7 @@
 
 #include "test_api.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace api;
 
@@ -81,4 +81,4 @@ TEST_F(TestApiWhiteTerm, getOp)
   ASSERT_EQ(tailTerm.getOp(), Op(&d_solver, APPLY_SELECTOR));
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/base/map_util_black.cpp b/test/unit/base/map_util_black.cpp
index 76238ad04..3ba866f30 100644
--- a/test/unit/base/map_util_black.cpp
+++ b/test/unit/base/map_util_black.cpp
@@ -27,7 +27,7 @@
 #include "context/context.h"
 #include "test.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using context::CDHashMap;
 using context::CDInsertHashMap;
@@ -63,8 +63,8 @@ class TestBaseBlackMap : public TestInternal
 TEST_F(TestBaseBlackMap, map)
 {
   std::map<std::string, std::string> map = default_map();
-  ASSERT_TRUE(CVC5::ContainsKey(map, "key"));
-  ASSERT_FALSE(CVC5::ContainsKey(map, "non key"));
+  ASSERT_TRUE(cvc5::ContainsKey(map, "key"));
+  ASSERT_FALSE(cvc5::ContainsKey(map, "non key"));
 
   ASSERT_EQ(FindOrNull(map, "non key"), nullptr);
   if (std::string* found_value = FindOrNull(map, "other"))
@@ -78,8 +78,8 @@ TEST_F(TestBaseBlackMap, map)
 TEST_F(TestBaseBlackMap, constant_map)
 {
   const std::map<std::string, std::string> map = default_map();
-  ASSERT_TRUE(CVC5::ContainsKey(map, "key"));
-  ASSERT_FALSE(CVC5::ContainsKey(map, "non key"));
+  ASSERT_TRUE(cvc5::ContainsKey(map, "key"));
+  ASSERT_FALSE(cvc5::ContainsKey(map, "non key"));
 
   if (const std::string* found_value = FindOrNull(map, "other"))
   {
@@ -94,8 +94,8 @@ TEST_F(TestBaseBlackMap, unordered_map)
 {
   std::unordered_map<std::string, std::string> map(default_map().begin(),
                                                    default_map().end());
-  ASSERT_TRUE(CVC5::ContainsKey(map, "key"));
-  ASSERT_FALSE(CVC5::ContainsKey(map, "non key"));
+  ASSERT_TRUE(cvc5::ContainsKey(map, "key"));
+  ASSERT_FALSE(cvc5::ContainsKey(map, "non key"));
 
   ASSERT_EQ(FindOrNull(map, "non key"), nullptr);
   if (std::string* found_value = FindOrNull(map, "other"))
@@ -110,8 +110,8 @@ TEST_F(TestBaseBlackMap, const_unordered_map)
 {
   const std::unordered_map<std::string, std::string> map(default_map().begin(),
                                                          default_map().end());
-  ASSERT_TRUE(CVC5::ContainsKey(map, "key"));
-  ASSERT_FALSE(CVC5::ContainsKey(map, "non key"));
+  ASSERT_TRUE(cvc5::ContainsKey(map, "key"));
+  ASSERT_FALSE(cvc5::ContainsKey(map, "non key"));
 
   if (const std::string* found_value = FindOrNull(map, "other"))
   {
@@ -125,23 +125,23 @@ TEST_F(TestBaseBlackMap, const_unordered_map)
 TEST_F(TestBaseBlackMap, set)
 {
   std::set<std::string> set{"entry", "other"};
-  ASSERT_TRUE(CVC5::ContainsKey(set, "entry"));
-  ASSERT_FALSE(CVC5::ContainsKey(set, "non member"));
+  ASSERT_TRUE(cvc5::ContainsKey(set, "entry"));
+  ASSERT_FALSE(cvc5::ContainsKey(set, "non member"));
 
   const std::set<std::string> const_set{"entry", "other"};
-  ASSERT_TRUE(CVC5::ContainsKey(const_set, "entry"));
-  ASSERT_FALSE(CVC5::ContainsKey(const_set, "non member"));
+  ASSERT_TRUE(cvc5::ContainsKey(const_set, "entry"));
+  ASSERT_FALSE(cvc5::ContainsKey(const_set, "non member"));
 }
 
 TEST_F(TestBaseBlackMap, unordered_set)
 {
   std::unordered_set<std::string> set{"entry", "other"};
-  ASSERT_TRUE(CVC5::ContainsKey(set, "entry"));
-  ASSERT_FALSE(CVC5::ContainsKey(set, "non member"));
+  ASSERT_TRUE(cvc5::ContainsKey(set, "entry"));
+  ASSERT_FALSE(cvc5::ContainsKey(set, "non member"));
 
   const std::unordered_set<std::string> const_set{"entry", "other"};
-  ASSERT_TRUE(CVC5::ContainsKey(const_set, "entry"));
-  ASSERT_FALSE(CVC5::ContainsKey(const_set, "non member"));
+  ASSERT_TRUE(cvc5::ContainsKey(const_set, "entry"));
+  ASSERT_FALSE(cvc5::ContainsKey(const_set, "non member"));
 }
 
 TEST_F(TestBaseBlackMap, CDHashMap)
@@ -150,8 +150,8 @@ TEST_F(TestBaseBlackMap, CDHashMap)
   CDHashMap<std::string, std::string> map(&context);
   insert_all(default_map(), &map);
 
-  ASSERT_TRUE(CVC5::ContainsKey(map, "key"));
-  ASSERT_FALSE(CVC5::ContainsKey(map, "non key"));
+  ASSERT_TRUE(cvc5::ContainsKey(map, "key"));
+  ASSERT_FALSE(cvc5::ContainsKey(map, "non key"));
 
   if (const std::string* found_value = FindOrNull(map, "other"))
   {
@@ -168,8 +168,8 @@ TEST_F(TestBaseBlackMap, const_CDHashMap)
   insert_all(default_map(), &store);
   const auto& map = store;
 
-  ASSERT_TRUE(CVC5::ContainsKey(map, "key"));
-  ASSERT_FALSE(CVC5::ContainsKey(map, "non key"));
+  ASSERT_TRUE(cvc5::ContainsKey(map, "key"));
+  ASSERT_FALSE(cvc5::ContainsKey(map, "non key"));
 
   if (const std::string* found_value = FindOrNull(map, "other"))
   {
@@ -185,8 +185,8 @@ TEST_F(TestBaseBlackMap, CDInsertHashMap)
   CDInsertHashMap<std::string, std::string> map(&context);
   insert_all(default_map(), &map);
 
-  ASSERT_TRUE(CVC5::ContainsKey(map, "key"));
-  ASSERT_FALSE(CVC5::ContainsKey(map, "non key"));
+  ASSERT_TRUE(cvc5::ContainsKey(map, "key"));
+  ASSERT_FALSE(cvc5::ContainsKey(map, "non key"));
 
   if (const std::string* found_value = FindOrNull(map, "other"))
   {
@@ -203,8 +203,8 @@ TEST_F(TestBaseBlackMap, const_CDInsertHashMap)
   insert_all(default_map(), &store);
   const auto& map = store;
 
-  ASSERT_TRUE(CVC5::ContainsKey(map, "key"));
-  ASSERT_FALSE(CVC5::ContainsKey(map, "non key"));
+  ASSERT_TRUE(cvc5::ContainsKey(map, "key"));
+  ASSERT_FALSE(cvc5::ContainsKey(map, "non key"));
   if (const std::string* found_value = FindOrNull(map, "other"))
   {
     ASSERT_EQ(*found_value, "entry");
@@ -213,4 +213,4 @@ TEST_F(TestBaseBlackMap, const_CDInsertHashMap)
   ASSERT_EQ(FindOrDie(map, "other"), "entry");
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/context/cdhashmap_black.cpp b/test/unit/context/cdhashmap_black.cpp
index 51d76070a..fbeae85b5 100644
--- a/test/unit/context/cdhashmap_black.cpp
+++ b/test/unit/context/cdhashmap_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::context::CDMap<>.
+ ** \brief Black box testing of cvc5::context::CDMap<>.
  **
- ** Black box testing of CVC5::context::CDMap<>.
+ ** Black box testing of cvc5::context::CDMap<>.
  **/
 
 #include <map>
@@ -21,11 +21,11 @@
 #include "context/cdlist.h"
 #include "test_context.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
-using CVC5::context::CDHashMap;
-using CVC5::context::Context;
+using cvc5::context::CDHashMap;
+using cvc5::context::Context;
 
 class TestContextBlackCDHashMap : public TestContext
 {
@@ -203,4 +203,4 @@ TEST_F(TestContextBlackCDHashMap, insert_at_context_level_zero)
   ASSERT_TRUE(elements_are(map, {{3, 4}, {23, 317}}));
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/context/cdhashmap_white.cpp b/test/unit/context/cdhashmap_white.cpp
index 06bcd8d46..72e437250 100644
--- a/test/unit/context/cdhashmap_white.cpp
+++ b/test/unit/context/cdhashmap_white.cpp
@@ -9,16 +9,16 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief White box testing of CVC5::context::CDMap<>.
+ ** \brief White box testing of cvc5::context::CDMap<>.
  **
- ** White box testing of CVC5::context::CDMap<>.
+ ** White box testing of cvc5::context::CDMap<>.
  **/
 
 #include "base/check.h"
 #include "context/cdhashmap.h"
 #include "test_context.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace context;
 
@@ -44,4 +44,4 @@ TEST_F(TestContextWhiteCDHashMap, unreachable_save_and_restore)
 }
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/context/cdlist_black.cpp b/test/unit/context/cdlist_black.cpp
index e903492ee..a3241d058 100644
--- a/test/unit/context/cdlist_black.cpp
+++ b/test/unit/context/cdlist_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::context::CDList<>.
+ ** \brief Black box testing of cvc5::context::CDList<>.
  **
- ** Black box testing of CVC5::context::CDList<>.
+ ** Black box testing of cvc5::context::CDList<>.
  **/
 
 #include <limits.h>
@@ -24,7 +24,7 @@
 #include "memory.h"
 #include "test_context.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace context;
 
@@ -163,4 +163,4 @@ TEST_F(TestContextBlackCDList, pop_below_level_created)
   list.push_back(42);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/context/cdo_black.cpp b/test/unit/context/cdo_black.cpp
index 033e60f57..c4e9b8dd5 100644
--- a/test/unit/context/cdo_black.cpp
+++ b/test/unit/context/cdo_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::context::CDO<>.
+ ** \brief Black box testing of cvc5::context::CDO<>.
  **
- ** Black box testing of CVC5::context::CDO<>.
+ ** Black box testing of cvc5::context::CDO<>.
  **/
 
 #include <iostream>
@@ -22,7 +22,7 @@
 #include "context/cdo.h"
 #include "test_context.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace context;
 
@@ -48,4 +48,4 @@ TEST_F(TestContextBlackCDO, cdo)
 }
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/context/context_black.cpp b/test/unit/context/context_black.cpp
index 7ec7ef6c8..0ad830162 100644
--- a/test/unit/context/context_black.cpp
+++ b/test/unit/context/context_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::context::Context.
+ ** \brief Black box testing of cvc5::context::Context.
  **
- ** Black box testing of CVC5::context::Context.
+ ** Black box testing of cvc5::context::Context.
  **/
 
 #include <iostream>
@@ -22,7 +22,7 @@
 #include "context/cdo.h"
 #include "test_context.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace context;
 
@@ -241,4 +241,4 @@ TEST_F(TestContextBlack, top_scope_context_obj)
 #endif
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/context/context_mm_black.cpp b/test/unit/context/context_mm_black.cpp
index 2dbec57b6..0f031ef5b 100644
--- a/test/unit/context/context_mm_black.cpp
+++ b/test/unit/context/context_mm_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::context::ContextMemoryManager.
+ ** \brief Black box testing of cvc5::context::ContextMemoryManager.
  **
- ** Black box testing of CVC5::context::ContextMemoryManager.
+ ** Black box testing of cvc5::context::ContextMemoryManager.
  **/
 
 #include <cstring>
@@ -21,7 +21,7 @@
 #include "context/context_mm.h"
 #include "test.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace context;
 
@@ -104,4 +104,4 @@ TEST_F(TestContextBlackMM, push_pop)
 }
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/context/context_white.cpp b/test/unit/context/context_white.cpp
index 6ec7ea3a1..7bda5d2da 100644
--- a/test/unit/context/context_white.cpp
+++ b/test/unit/context/context_white.cpp
@@ -9,16 +9,16 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief White box testing of CVC5::context::Context.
+ ** \brief White box testing of cvc5::context::Context.
  **
- ** White box testing of CVC5::context::Context.
+ ** White box testing of cvc5::context::Context.
  **/
 
 #include "base/check.h"
 #include "context/cdo.h"
 #include "test_context.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace context;
 
@@ -180,4 +180,4 @@ TEST_F(TestContextWhite, simple)
   ASSERT_EQ(c.d_ppContextObjPrev, &s->d_pContextObjList);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp
index 0ee485fc2..7ab337c09 100644
--- a/test/unit/main/interactive_shell_black.cpp
+++ b/test/unit/main/interactive_shell_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::InteractiveShell.
+ ** \brief Black box testing of cvc5::InteractiveShell.
  **
- ** Black box testing of CVC5::InteractiveShell.
+ ** Black box testing of cvc5::InteractiveShell.
  **/
 
 #include <sstream>
@@ -27,7 +27,7 @@
 #include "smt/command.h"
 #include "test.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestMainBlackInteractiveShell : public TestInternal
@@ -41,7 +41,7 @@ class TestMainBlackInteractiveShell : public TestInternal
     d_options.set(options::in, d_sin.get());
     d_options.set(options::out, d_sout.get());
     d_options.set(options::inputLanguage, language::input::LANG_CVC4);
-    d_solver.reset(new CVC5::api::Solver(&d_options));
+    d_solver.reset(new cvc5::api::Solver(&d_options));
     d_symman.reset(new SymbolManager(d_solver.get()));
   }
 
@@ -80,7 +80,7 @@ class TestMainBlackInteractiveShell : public TestInternal
   std::unique_ptr<std::stringstream> d_sin;
   std::unique_ptr<std::stringstream> d_sout;
   std::unique_ptr<SymbolManager> d_symman;
-  std::unique_ptr<CVC5::api::Solver> d_solver;
+  std::unique_ptr<cvc5::api::Solver> d_solver;
   Options d_options;
 };
 
@@ -133,4 +133,4 @@ TEST_F(TestMainBlackInteractiveShell, repeated_empty_lines)
   countCommands(shell, 0, 3);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/memory.h b/test/unit/memory.h
index 1341274dd..f9bdd7851 100644
--- a/test/unit/memory.h
+++ b/test/unit/memory.h
@@ -15,7 +15,7 @@
  **
  ** Use it like this (for example):
  **
- **   CVC5::test::WithLimitedMemory wlm(amount);
+ **   cvc5::test::WithLimitedMemory wlm(amount);
  **   TS_ASSERT_THROWS( foo(), bad_alloc );
  **
  ** The WithLimitedMemory destructor will re-establish the previous limit.
@@ -53,7 +53,7 @@
 #  endif
 #endif
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 #ifndef CVC4_MEMORY_LIMITING_DISABLED
@@ -87,7 +87,7 @@ class WithLimitedMemory {
 #endif
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
 
 // Remove CVC4_MEMORY_LIMITING_DISABLED_REASON if it is defined.
 #ifdef CVC4_MEMORY_LIMITING_DISABLED_REASON
diff --git a/test/unit/node/attribute_black.cpp b/test/unit/node/attribute_black.cpp
index 48f68159f..880bb85e4 100644
--- a/test/unit/node/attribute_black.cpp
+++ b/test/unit/node/attribute_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::Attribute.
+ ** \brief Black box testing of cvc5::Attribute.
  **
- ** Black box testing of CVC5::Attribute.
+ ** Black box testing of cvc5::Attribute.
  **/
 
 #include <sstream>
@@ -23,7 +23,7 @@
 #include "expr/node_value.h"
 #include "test_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 using namespace smt;
@@ -125,4 +125,4 @@ TEST_F(TestNodeBlackAttribute, bools)
 }
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/node/attribute_white.cpp b/test/unit/node/attribute_white.cpp
index 75bc87893..59d9500c7 100644
--- a/test/unit/node/attribute_white.cpp
+++ b/test/unit/node/attribute_white.cpp
@@ -30,7 +30,7 @@
 #include "theory/theory_engine.h"
 #include "theory/uf/theory_uf.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 using namespace smt;
@@ -445,4 +445,4 @@ TEST_F(TestNodeWhiteAttribute, attributes)
   ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr()));
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/node/kind_black.cpp b/test/unit/node/kind_black.cpp
index 9c497f026..defc3aa6f 100644
--- a/test/unit/node/kind_black.cpp
+++ b/test/unit/node/kind_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::Kind.
+ ** \brief Black box testing of cvc5::Kind.
  **
- ** Black box testing of CVC5::Kind.
+ ** Black box testing of cvc5::Kind.
  **/
 
 #include <iostream>
@@ -21,7 +21,7 @@
 #include "expr/kind.h"
 #include "test.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 
@@ -87,4 +87,4 @@ TEST_F(TestNodeBlackKind, output_concat)
   ASSERT_EQ(act.str(), exp.str());
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/node/kind_map_black.cpp b/test/unit/node/kind_map_black.cpp
index 85c8fb2cd..7da3e5715 100644
--- a/test/unit/node/kind_map_black.cpp
+++ b/test/unit/node/kind_map_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::KindMap
+ ** \brief Black box testing of cvc5::KindMap
  **
- ** Black box testing of CVC5::KindMap.
+ ** Black box testing of cvc5::KindMap.
  **/
 
 #include <iostream>
@@ -21,7 +21,7 @@
 #include "expr/kind_map.h"
 #include "test.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 
@@ -45,4 +45,4 @@ TEST_F(TestNodeBlackKindMap, simple)
 }
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp
index 47f66f0c3..b9cac2169 100644
--- a/test/unit/node/node_algorithm_black.cpp
+++ b/test/unit/node/node_algorithm_black.cpp
@@ -25,7 +25,7 @@
 #include "util/integer.h"
 #include "util/rational.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace expr;
 using namespace kind;
@@ -199,4 +199,4 @@ TEST_F(TestNodeBlackNodeAlgorithm, match)
   ASSERT_EQ(subs[x], a);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 7ae8a9434..5177ff453 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::Node.
+ ** \brief Black box testing of cvc5::Node.
  **
- ** Black box testing of CVC5::Node.
+ ** Black box testing of cvc5::Node.
  **/
 
 #include <algorithm>
@@ -30,7 +30,7 @@
 #include "test_node.h"
 #include "theory/rewriter.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 
@@ -784,4 +784,4 @@ TEST_F(TestNodeBlackNode, node_tnode_usage)
 }
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp
index 62410bcb7..39c5552df 100644
--- a/test/unit/node/node_builder_black.cpp
+++ b/test/unit/node/node_builder_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::NodeBuilder.
+ ** \brief Black box testing of cvc5::NodeBuilder.
  **
- ** Black box testing of CVC5::NodeBuilder.
+ ** Black box testing of cvc5::NodeBuilder.
  **/
 
 #include <limits.h>
@@ -30,7 +30,7 @@
 #define K 30u
 #define LARGE_K UINT_MAX / 40
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 
@@ -587,4 +587,4 @@ TEST_F(TestNodeBlackNodeBuilder, leftist_building)
   ASSERT_EQ(nexpected, n);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp
index 7866d87bd..5d21ff734 100644
--- a/test/unit/node/node_manager_black.cpp
+++ b/test/unit/node/node_manager_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::NodeManager.
+ ** \brief Black box testing of cvc5::NodeManager.
  **
- ** Black box testing of CVC5::NodeManager.
+ ** Black box testing of cvc5::NodeManager.
  **/
 
 #include <string>
@@ -24,7 +24,7 @@
 #include "util/integer.h"
 #include "util/rational.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 using namespace expr;
@@ -330,4 +330,4 @@ TEST_F(TestNodeBlackNodeManager, mkNode_too_many_children)
 #endif
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp
index 588c39181..dcdbc074f 100644
--- a/test/unit/node/node_manager_white.cpp
+++ b/test/unit/node/node_manager_white.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief White box testing of CVC5::NodeManager.
+ ** \brief White box testing of cvc5::NodeManager.
  **
- ** White box testing of CVC5::NodeManager.
+ ** White box testing of cvc5::NodeManager.
  **/
 
 #include <string>
@@ -21,9 +21,9 @@
 #include "util/integer.h"
 #include "util/rational.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
-using namespace CVC5::expr;
+using namespace cvc5::expr;
 
 namespace test {
 
@@ -81,4 +81,4 @@ TEST_F(TestNodeWhiteNodeManager, topological_sort)
   }
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/node/node_self_iterator_black.cpp b/test/unit/node/node_self_iterator_black.cpp
index 0a0a877c3..43eebcda9 100644
--- a/test/unit/node/node_self_iterator_black.cpp
+++ b/test/unit/node/node_self_iterator_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::expr::NodeSelfIterator
+ ** \brief Black box testing of cvc5::expr::NodeSelfIterator
  **
- ** Black box testing of CVC5::expr::NodeSelfIterator
+ ** Black box testing of cvc5::expr::NodeSelfIterator
  **/
 
 #include "expr/node.h"
@@ -19,7 +19,7 @@
 #include "expr/node_self_iterator.h"
 #include "test_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 using namespace expr;
@@ -54,4 +54,4 @@ TEST_F(TestNodeBlackNodeSelfIterator, iteration)
   ASSERT_EQ(++i, x_and_y.end());
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/node/node_traversal_black.cpp b/test/unit/node/node_traversal_black.cpp
index c54be86ac..8366b1a63 100644
--- a/test/unit/node/node_traversal_black.cpp
+++ b/test/unit/node/node_traversal_black.cpp
@@ -26,7 +26,7 @@
 #include "expr/node_value.h"
 #include "test_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 
@@ -293,4 +293,4 @@ TEST_F(TestNodeBlackNodeTraversalPreorder, skip_if)
   ASSERT_EQ(actual, expected);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp
index d914c5dc2..20de9d3e4 100644
--- a/test/unit/node/node_white.cpp
+++ b/test/unit/node/node_white.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief White box testing of CVC5::Node.
+ ** \brief White box testing of cvc5::Node.
  **
- ** White box testing of CVC5::Node.
+ ** White box testing of cvc5::Node.
  **/
 
 #include <string>
@@ -19,7 +19,7 @@
 #include "base/check.h"
 #include "test_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 using namespace expr;
@@ -79,4 +79,4 @@ TEST_F(TestNodeWhiteNode, iterators)
   ASSERT_EQ(v[2], y);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/node/symbol_table_black.cpp b/test/unit/node/symbol_table_black.cpp
index 27911c34b..7b01b520d 100644
--- a/test/unit/node/symbol_table_black.cpp
+++ b/test/unit/node/symbol_table_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::SymbolTable
+ ** \brief Black box testing of cvc5::SymbolTable
  **
- ** Black box testing of CVC5::SymbolTable.
+ ** Black box testing of cvc5::SymbolTable.
  **/
 
 #include <sstream>
@@ -24,7 +24,7 @@
 #include "expr/symbol_table.h"
 #include "test_api.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 using namespace context;
@@ -146,4 +146,4 @@ TEST_F(TestNodeBlackSymbolTable, bad_pop)
 }
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/node/type_cardinality_black.cpp b/test/unit/node/type_cardinality_black.cpp
index e2aeced08..f0ee99a7d 100644
--- a/test/unit/node/type_cardinality_black.cpp
+++ b/test/unit/node/type_cardinality_black.cpp
@@ -21,7 +21,7 @@
 #include "test_node.h"
 #include "util/cardinality.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 
@@ -332,4 +332,4 @@ TEST_F(TestNodeBlackTypeCardinality, bitvectors)
 }
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp
index 37d80a9fa..c6f862e03 100644
--- a/test/unit/node/type_node_white.cpp
+++ b/test/unit/node/type_node_white.cpp
@@ -23,7 +23,7 @@
 #include "smt/smt_engine.h"
 #include "test_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 using namespace context;
@@ -94,4 +94,4 @@ TEST_F(TestNodeWhiteTypeNode, sub_types)
   ASSERT_TRUE(bvType.getBaseType() == bvType);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp
index 827d7dd84..3c6d8b820 100644
--- a/test/unit/parser/parser_black.cpp
+++ b/test/unit/parser/parser_black.cpp
@@ -9,10 +9,10 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::parser::Parser for CVC and SMT-LIBv2
+ ** \brief Black box testing of cvc5::parser::Parser for CVC and SMT-LIBv2
  ** inputs.
  **
- ** Black box testing of CVC5::parser::Parser for CVC and SMT-LIbv2 inputs.
+ ** Black box testing of cvc5::parser::Parser for CVC and SMT-LIbv2 inputs.
  **/
 
 #include <sstream>
@@ -29,7 +29,7 @@
 #include "smt/command.h"
 #include "test.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace parser;
 using namespace language::input;
@@ -48,7 +48,7 @@ class TestParserBlackParser : public TestInternal
     TestInternal::SetUp();
     d_options.set(options::parseOnly, true);
     d_symman.reset(nullptr);
-    d_solver.reset(new CVC5::api::Solver(&d_options));
+    d_solver.reset(new cvc5::api::Solver(&d_options));
   }
 
   void TearDown() override
@@ -186,7 +186,7 @@ class TestParserBlackParser : public TestInternal
 
   Options d_options;
   InputLanguage d_lang;
-  std::unique_ptr<CVC5::api::Solver> d_solver;
+  std::unique_ptr<cvc5::api::Solver> d_solver;
   std::unique_ptr<SymbolManager> d_symman;
 };
 
@@ -392,4 +392,4 @@ TEST_F(TestParserBlackSmt2Parser, bad_exprs)
 #endif
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/parser/parser_builder_black.cpp b/test/unit/parser/parser_builder_black.cpp
index 3ebd11b83..a83932b2f 100644
--- a/test/unit/parser/parser_builder_black.cpp
+++ b/test/unit/parser/parser_builder_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::parser::ParserBuilder.
+ ** \brief Black box testing of cvc5::parser::ParserBuilder.
  **
- ** Black box testing of CVC5::parser::ParserBuilder.
+ ** Black box testing of cvc5::parser::ParserBuilder.
  **/
 
 #include <stdio.h>
@@ -29,7 +29,7 @@
 #include "parser/parser_builder.h"
 #include "test_api.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace parser;
 using namespace language::input;
@@ -134,4 +134,4 @@ TEST_F(TestParseBlackParserBuilder, true_stream_input)
 }
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp
index 130d6b1cf..d313e01c7 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.cpp
+++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp
@@ -29,7 +29,7 @@
 #include "theory/rewriter.h"
 #include "util/bitvector.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace preprocessing;
 using namespace preprocessing::passes;
@@ -3099,4 +3099,4 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw5b)
   ASSERT_EQ(BVGauss::getMinBwExpr(Rewriter::rewrite(plus7)), 17);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp
index cbd178576..662a53777 100644
--- a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp
+++ b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp
@@ -18,7 +18,7 @@
 #include "smt/smt_engine.h"
 #include "test_smt.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace preprocessing::passes;
 
@@ -47,4 +47,4 @@ TEST_F(TestPPWhiteForeignTheoryRewrite, simplify)
 }
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/printer/smt2_printer_black.cpp b/test/unit/printer/smt2_printer_black.cpp
index 2f4d6fb38..03ab95083 100644
--- a/test/unit/printer/smt2_printer_black.cpp
+++ b/test/unit/printer/smt2_printer_black.cpp
@@ -23,7 +23,7 @@
 #include "smt/smt_engine.h"
 #include "test_smt.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 
@@ -59,4 +59,4 @@ TEST_F(TestPrinterBlackSmt2, regexp_loop)
   checkToString(n, "((_ re.loop 1 3) (str.to_re \"x\"))");
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/prop/cnf_stream_white.cpp b/test/unit/prop/cnf_stream_white.cpp
index 40f986d33..0529f209c 100644
--- a/test/unit/prop/cnf_stream_white.cpp
+++ b/test/unit/prop/cnf_stream_white.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief White box testing of CVC5::prop::CnfStream.
+ ** \brief White box testing of cvc5::prop::CnfStream.
  **
- ** White box testing of CVC5::prop::CnfStream.
+ ** White box testing of cvc5::prop::CnfStream.
  **/
 
 #include "base/check.h"
@@ -28,7 +28,7 @@
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace context;
 using namespace prop;
@@ -113,7 +113,7 @@ class TestPropWhiteCnfStream : public TestSmt
     d_cnfContext.reset(new context::Context());
     d_cnfRegistrar.reset(new prop::NullRegistrar);
     d_cnfStream.reset(
-        new CVC5::prop::CnfStream(d_satSolver.get(),
+        new cvc5::prop::CnfStream(d_satSolver.get(),
                                   d_cnfRegistrar.get(),
                                   d_cnfContext.get(),
                                   &d_smtEngine->getOutputManager(),
@@ -271,4 +271,4 @@ TEST_F(TestPropWhiteCnfStream, ensure_literal)
   ASSERT_TRUE(d_cnfStream->hasLiteral(a_and_b));
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/test.h b/test/unit/test.h
index 1c5614488..11cefc66b 100644
--- a/test/unit/test.h
+++ b/test/unit/test.h
@@ -17,7 +17,7 @@
 
 #include "gtest/gtest.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestInternal : public ::testing::Test
@@ -25,5 +25,5 @@ class TestInternal : public ::testing::Test
 };
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
 #endif
diff --git a/test/unit/test_api.h b/test/unit/test_api.h
index 033136524..7ad2e1e5c 100644
--- a/test/unit/test_api.h
+++ b/test/unit/test_api.h
@@ -18,15 +18,15 @@
 #include "api/cvc4cpp.h"
 #include "gtest/gtest.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestApi : public ::testing::Test
 {
  protected:
-  CVC5::api::Solver d_solver;
+  cvc5::api::Solver d_solver;
 };
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
 #endif
diff --git a/test/unit/test_context.h b/test/unit/test_context.h
index 024488fc4..0f21b2898 100644
--- a/test/unit/test_context.h
+++ b/test/unit/test_context.h
@@ -18,16 +18,16 @@
 #include "context/context.h"
 #include "test.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestContext : public TestInternal
 {
  protected:
-  void SetUp() override { d_context.reset(new CVC5::context::Context()); }
-  std::unique_ptr<CVC5::context::Context> d_context;
+  void SetUp() override { d_context.reset(new cvc5::context::Context()); }
+  std::unique_ptr<cvc5::context::Context> d_context;
 };
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
 #endif
diff --git a/test/unit/test_node.h b/test/unit/test_node.h
index 1aefbae45..359cc0b6f 100644
--- a/test/unit/test_node.h
+++ b/test/unit/test_node.h
@@ -20,7 +20,7 @@
 #include "smt/smt_engine_scope.h"
 #include "test.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestNode : public TestInternal
@@ -45,5 +45,5 @@ class TestNode : public TestInternal
 };
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
 #endif
diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h
index a6097b56c..a26e039e4 100644
--- a/test/unit/test_smt.h
+++ b/test/unit/test_smt.h
@@ -29,7 +29,7 @@
 #include "util/resource_manager.h"
 #include "util/unsafe_interrupt_exception.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 /* -------------------------------------------------------------------------- */
@@ -99,7 +99,7 @@ inline std::ostream& operator<<(std::ostream& out, OutputChannelCallType type)
   }
 }
 
-class DummyOutputChannel : public CVC5::theory::OutputChannel
+class DummyOutputChannel : public cvc5::theory::OutputChannel
 {
  public:
   DummyOutputChannel() {}
@@ -249,5 +249,5 @@ class DummyTheory : public theory::Theory
 
 /* -------------------------------------------------------------------------- */
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
 #endif
diff --git a/test/unit/theory/evaluator_white.cpp b/test/unit/theory/evaluator_white.cpp
index 54976c7d7..2afaf3a48 100644
--- a/test/unit/theory/evaluator_white.cpp
+++ b/test/unit/theory/evaluator_white.cpp
@@ -24,7 +24,7 @@
 #include "theory/rewriter.h"
 #include "util/rational.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace theory;
 
@@ -156,4 +156,4 @@ TEST_F(TestTheoryWhiteEvaluator, code)
   }
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/logic_info_white.cpp b/test/unit/theory/logic_info_white.cpp
index 0c45cc4ed..5c18b7c98 100644
--- a/test/unit/theory/logic_info_white.cpp
+++ b/test/unit/theory/logic_info_white.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Unit testing for CVC5::LogicInfo class
+ ** \brief Unit testing for cvc5::LogicInfo class
  **
- ** Unit testing for CVC5::LogicInfo class.
+ ** Unit testing for cvc5::LogicInfo class.
  **/
 
 #include "base/configuration.h"
@@ -19,7 +19,7 @@
 #include "test.h"
 #include "theory/logic_info.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace theory;
 
@@ -544,33 +544,33 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic)
   LogicInfo info;
   ASSERT_FALSE(info.isLocked());
 
-  ASSERT_THROW(info.getLogicString(), CVC5::IllegalArgumentException);
+  ASSERT_THROW(info.getLogicString(), cvc5::IllegalArgumentException);
   ASSERT_THROW(info.isTheoryEnabled(THEORY_BUILTIN),
-               CVC5::IllegalArgumentException);
+               cvc5::IllegalArgumentException);
   ASSERT_THROW(info.isTheoryEnabled(THEORY_BOOL),
-               CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.isTheoryEnabled(THEORY_UF), CVC5::IllegalArgumentException);
+               cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.isTheoryEnabled(THEORY_UF), cvc5::IllegalArgumentException);
   ASSERT_THROW(info.isTheoryEnabled(THEORY_ARITH),
-               CVC5::IllegalArgumentException);
+               cvc5::IllegalArgumentException);
   ASSERT_THROW(info.isTheoryEnabled(THEORY_ARRAYS),
-               CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.isTheoryEnabled(THEORY_BV), CVC5::IllegalArgumentException);
+               cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.isTheoryEnabled(THEORY_BV), cvc5::IllegalArgumentException);
   ASSERT_THROW(info.isTheoryEnabled(THEORY_DATATYPES),
-               CVC5::IllegalArgumentException);
+               cvc5::IllegalArgumentException);
   ASSERT_THROW(info.isTheoryEnabled(THEORY_QUANTIFIERS),
-               CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.isPure(THEORY_BUILTIN), CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.isPure(THEORY_BOOL), CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.isPure(THEORY_UF), CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.isPure(THEORY_ARITH), CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.isPure(THEORY_ARRAYS), CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.isPure(THEORY_BV), CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.isPure(THEORY_DATATYPES), CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.isPure(THEORY_QUANTIFIERS), CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.isQuantified(), CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.areIntegersUsed(), CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.areRealsUsed(), CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.isLinear(), CVC5::IllegalArgumentException);
+               cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.isPure(THEORY_BUILTIN), cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.isPure(THEORY_BOOL), cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.isPure(THEORY_UF), cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.isPure(THEORY_ARITH), cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.isPure(THEORY_ARRAYS), cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.isPure(THEORY_BV), cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.isPure(THEORY_DATATYPES), cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.isPure(THEORY_QUANTIFIERS), cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.isQuantified(), cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.areIntegersUsed(), cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.areRealsUsed(), cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.isLinear(), cvc5::IllegalArgumentException);
 
   info.lock();
   ASSERT_TRUE(info.isLocked());
@@ -598,17 +598,17 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic)
   ASSERT_TRUE(info.areTranscendentalsUsed());
   ASSERT_FALSE(info.isLinear());
 
-  ASSERT_THROW(info.arithOnlyLinear(), CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.disableIntegers(), CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.disableQuantifiers(), CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.disableTheory(THEORY_BV), CVC5::IllegalArgumentException);
+  ASSERT_THROW(info.arithOnlyLinear(), cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.disableIntegers(), cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.disableQuantifiers(), cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.disableTheory(THEORY_BV), cvc5::IllegalArgumentException);
   ASSERT_THROW(info.disableTheory(THEORY_DATATYPES),
-               CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.enableIntegers(), CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.disableReals(), CVC5::IllegalArgumentException);
+               cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.enableIntegers(), cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.disableReals(), cvc5::IllegalArgumentException);
   ASSERT_THROW(info.disableTheory(THEORY_ARITH),
-               CVC5::IllegalArgumentException);
-  ASSERT_THROW(info.disableTheory(THEORY_UF), CVC5::IllegalArgumentException);
+               cvc5::IllegalArgumentException);
+  ASSERT_THROW(info.disableTheory(THEORY_UF), cvc5::IllegalArgumentException);
   info = info.getUnlockedCopy();
   ASSERT_FALSE(info.isLocked());
   info.disableTheory(THEORY_STRINGS);
@@ -617,7 +617,7 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic)
   info.arithOnlyLinear();
   info.disableIntegers();
   info.lock();
-  if (CVC5::Configuration::isBuiltWithSymFPU())
+  if (cvc5::Configuration::isBuiltWithSymFPU())
   {
     ASSERT_EQ(info.getLogicString(), "SEP_AUFBVFPDTLRA");
   }
@@ -631,7 +631,7 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic)
   info.disableQuantifiers();
   info.disableTheory(THEORY_BAGS);
   info.lock();
-  if (CVC5::Configuration::isBuiltWithSymFPU())
+  if (cvc5::Configuration::isBuiltWithSymFPU())
   {
     ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFBVFPDTLRA");
   }
@@ -648,7 +648,7 @@ TEST_F(TestTheoryWhiteLogicInfo, default_logic)
   info.enableIntegers();
   info.disableReals();
   info.lock();
-  if (CVC5::Configuration::isBuiltWithSymFPU())
+  if (cvc5::Configuration::isBuiltWithSymFPU())
   {
     ASSERT_EQ(info.getLogicString(), "QF_SEP_AUFFPLIA");
   }
@@ -1371,4 +1371,4 @@ TEST_F(TestTheoryWhiteLogicInfo, comparison)
   gt(ufHo, "QF_UF");
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/regexp_operation_black.cpp b/test/unit/theory/regexp_operation_black.cpp
index b87701534..ed432ca2f 100644
--- a/test/unit/theory/regexp_operation_black.cpp
+++ b/test/unit/theory/regexp_operation_black.cpp
@@ -27,7 +27,7 @@
 #include "theory/strings/regexp_operation.h"
 #include "theory/strings/skolem_cache.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 using namespace theory;
@@ -144,4 +144,4 @@ TEST_F(TestTheoryBlackRegexpOperation, star_wildcards)
 }
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp
index 7a85ad13d..a1512d7de 100644
--- a/test/unit/theory/sequences_rewriter_white.cpp
+++ b/test/unit/theory/sequences_rewriter_white.cpp
@@ -28,7 +28,7 @@
 #include "theory/strings/strings_entail.h"
 #include "theory/strings/strings_rewriter.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace theory;
 using namespace theory::quantifiers;
@@ -85,10 +85,10 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_length_one)
   TypeNode intType = d_nodeManager->integerType();
   TypeNode strType = d_nodeManager->stringType();
 
-  Node a = d_nodeManager->mkConst(::CVC5::String("A"));
-  Node abcd = d_nodeManager->mkConst(::CVC5::String("ABCD"));
-  Node aaad = d_nodeManager->mkConst(::CVC5::String("AAAD"));
-  Node b = d_nodeManager->mkConst(::CVC5::String("B"));
+  Node a = d_nodeManager->mkConst(::cvc5::String("A"));
+  Node abcd = d_nodeManager->mkConst(::cvc5::String("ABCD"));
+  Node aaad = d_nodeManager->mkConst(::cvc5::String("AAAD"));
+  Node b = d_nodeManager->mkConst(::cvc5::String("B"));
   Node x = d_nodeManager->mkVar("x", strType);
   Node y = d_nodeManager->mkVar("y", strType);
   Node negOne = d_nodeManager->mkConst(Rational(-1));
@@ -149,8 +149,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, check_entail_with_with_assumption)
   Node zero = d_nodeManager->mkConst(Rational(0));
   Node one = d_nodeManager->mkConst(Rational(1));
 
-  Node empty = d_nodeManager->mkConst(::CVC5::String(""));
-  Node a = d_nodeManager->mkConst(::CVC5::String("A"));
+  Node empty = d_nodeManager->mkConst(::cvc5::String(""));
+  Node a = d_nodeManager->mkConst(::cvc5::String("A"));
 
   Node slen_y = d_nodeManager->mkNode(kind::STRING_LENGTH, y);
   Node x_plus_slen_y = d_nodeManager->mkNode(kind::PLUS, x, slen_y);
@@ -223,10 +223,10 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_substr)
   TypeNode intType = d_nodeManager->integerType();
   TypeNode strType = d_nodeManager->stringType();
 
-  Node empty = d_nodeManager->mkConst(::CVC5::String(""));
-  Node a = d_nodeManager->mkConst(::CVC5::String("A"));
-  Node b = d_nodeManager->mkConst(::CVC5::String("B"));
-  Node abcd = d_nodeManager->mkConst(::CVC5::String("ABCD"));
+  Node empty = d_nodeManager->mkConst(::cvc5::String(""));
+  Node a = d_nodeManager->mkConst(::cvc5::String("A"));
+  Node b = d_nodeManager->mkConst(::cvc5::String("B"));
+  Node abcd = d_nodeManager->mkConst(::cvc5::String("ABCD"));
   Node negone = d_nodeManager->mkConst(Rational(-1));
   Node zero = d_nodeManager->mkConst(Rational(0));
   Node one = d_nodeManager->mkConst(Rational(1));
@@ -364,8 +364,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_concat)
   TypeNode intType = d_nodeManager->integerType();
   TypeNode strType = d_nodeManager->stringType();
 
-  Node empty = d_nodeManager->mkConst(::CVC5::String(""));
-  Node a = d_nodeManager->mkConst(::CVC5::String("A"));
+  Node empty = d_nodeManager->mkConst(::cvc5::String(""));
+  Node a = d_nodeManager->mkConst(::cvc5::String("A"));
   Node zero = d_nodeManager->mkConst(Rational(0));
   Node three = d_nodeManager->mkConst(Rational(3));
 
@@ -431,11 +431,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, length_preserve_rewrite)
   TypeNode intType = d_nodeManager->integerType();
   TypeNode strType = d_nodeManager->stringType();
 
-  Node empty = d_nodeManager->mkConst(::CVC5::String(""));
-  Node abcd = d_nodeManager->mkConst(::CVC5::String("ABCD"));
-  Node f = d_nodeManager->mkConst(::CVC5::String("F"));
-  Node gh = d_nodeManager->mkConst(::CVC5::String("GH"));
-  Node ij = d_nodeManager->mkConst(::CVC5::String("IJ"));
+  Node empty = d_nodeManager->mkConst(::cvc5::String(""));
+  Node abcd = d_nodeManager->mkConst(::cvc5::String("ABCD"));
+  Node f = d_nodeManager->mkConst(::cvc5::String("F"));
+  Node gh = d_nodeManager->mkConst(::cvc5::String("GH"));
+  Node ij = d_nodeManager->mkConst(::cvc5::String("IJ"));
 
   Node i = d_nodeManager->mkVar("i", intType);
   Node s = d_nodeManager->mkVar("s", strType);
@@ -467,12 +467,12 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_indexOf)
   TypeNode intType = d_nodeManager->integerType();
   TypeNode strType = d_nodeManager->stringType();
 
-  Node a = d_nodeManager->mkConst(::CVC5::String("A"));
-  Node abcd = d_nodeManager->mkConst(::CVC5::String("ABCD"));
-  Node aaad = d_nodeManager->mkConst(::CVC5::String("AAAD"));
-  Node b = d_nodeManager->mkConst(::CVC5::String("B"));
-  Node c = d_nodeManager->mkConst(::CVC5::String("C"));
-  Node ccc = d_nodeManager->mkConst(::CVC5::String("CCC"));
+  Node a = d_nodeManager->mkConst(::cvc5::String("A"));
+  Node abcd = d_nodeManager->mkConst(::cvc5::String("ABCD"));
+  Node aaad = d_nodeManager->mkConst(::cvc5::String("AAAD"));
+  Node b = d_nodeManager->mkConst(::cvc5::String("B"));
+  Node c = d_nodeManager->mkConst(::cvc5::String("C"));
+  Node ccc = d_nodeManager->mkConst(::cvc5::String("CCC"));
   Node x = d_nodeManager->mkVar("x", strType);
   Node y = d_nodeManager->mkVar("y", strType);
   Node negOne = d_nodeManager->mkConst(Rational(-1));
@@ -577,12 +577,12 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace)
   TypeNode intType = d_nodeManager->integerType();
   TypeNode strType = d_nodeManager->stringType();
 
-  Node empty = d_nodeManager->mkConst(::CVC5::String(""));
-  Node a = d_nodeManager->mkConst(::CVC5::String("A"));
-  Node ab = d_nodeManager->mkConst(::CVC5::String("AB"));
-  Node b = d_nodeManager->mkConst(::CVC5::String("B"));
-  Node c = d_nodeManager->mkConst(::CVC5::String("C"));
-  Node d = d_nodeManager->mkConst(::CVC5::String("D"));
+  Node empty = d_nodeManager->mkConst(::cvc5::String(""));
+  Node a = d_nodeManager->mkConst(::cvc5::String("A"));
+  Node ab = d_nodeManager->mkConst(::cvc5::String("AB"));
+  Node b = d_nodeManager->mkConst(::cvc5::String("B"));
+  Node c = d_nodeManager->mkConst(::cvc5::String("C"));
+  Node d = d_nodeManager->mkConst(::cvc5::String("D"));
   Node x = d_nodeManager->mkVar("x", strType);
   Node y = d_nodeManager->mkVar("y", strType);
   Node z = d_nodeManager->mkVar("z", strType);
@@ -773,7 +773,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re)
                                    d_nodeManager->mkConst(String("AZZZB")),
                                    re,
                                    foo);
-    Node res = d_nodeManager->mkConst(::CVC5::String("FOO"));
+    Node res = d_nodeManager->mkConst(::cvc5::String("FOO"));
     sameNormalForm(t, res);
   }
 
@@ -790,7 +790,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re)
                                    d_nodeManager->mkConst(String("ZAZZZBZZB")),
                                    re,
                                    foo);
-    Node res = d_nodeManager->mkConst(::CVC5::String("ZFOOZZB"));
+    Node res = d_nodeManager->mkConst(::cvc5::String("ZFOOZZB"));
     sameNormalForm(t, res);
   }
 
@@ -807,7 +807,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re)
                                    d_nodeManager->mkConst(String("ZAZZZBZAZB")),
                                    re,
                                    foo);
-    Node res = d_nodeManager->mkConst(::CVC5::String("ZFOOZAZB"));
+    Node res = d_nodeManager->mkConst(::cvc5::String("ZFOOZAZB"));
     sameNormalForm(t, res);
   }
 
@@ -824,7 +824,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re)
                                    d_nodeManager->mkConst(String("ZZZ")),
                                    re,
                                    foo);
-    Node res = d_nodeManager->mkConst(::CVC5::String("ZZZ"));
+    Node res = d_nodeManager->mkConst(::cvc5::String("ZZZ"));
     sameNormalForm(t, res);
   }
 
@@ -841,7 +841,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re)
                                    d_nodeManager->mkConst(String("ZZZ")),
                                    sigStar,
                                    foo);
-    Node res = d_nodeManager->mkConst(::CVC5::String("FOOZZZ"));
+    Node res = d_nodeManager->mkConst(::cvc5::String("FOOZZZ"));
     sameNormalForm(t, res);
   }
 
@@ -858,7 +858,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_re)
                                    d_nodeManager->mkConst(String("")),
                                    sigStar,
                                    foo);
-    Node res = d_nodeManager->mkConst(::CVC5::String("FOO"));
+    Node res = d_nodeManager->mkConst(::cvc5::String("FOO"));
     sameNormalForm(t, res);
   }
 }
@@ -893,7 +893,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all)
                                    d_nodeManager->mkConst(String("AZZZB")),
                                    re,
                                    foo);
-    Node res = d_nodeManager->mkConst(::CVC5::String("FOO"));
+    Node res = d_nodeManager->mkConst(::cvc5::String("FOO"));
     sameNormalForm(t, res);
   }
 
@@ -910,7 +910,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all)
                                    d_nodeManager->mkConst(String("ZAZZZBZZB")),
                                    re,
                                    foo);
-    Node res = d_nodeManager->mkConst(::CVC5::String("ZFOOZZB"));
+    Node res = d_nodeManager->mkConst(::cvc5::String("ZFOOZZB"));
     sameNormalForm(t, res);
   }
 
@@ -927,7 +927,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all)
                                    d_nodeManager->mkConst(String("ZAZZZBZAZB")),
                                    re,
                                    foo);
-    Node res = d_nodeManager->mkConst(::CVC5::String("ZFOOZFOO"));
+    Node res = d_nodeManager->mkConst(::cvc5::String("ZFOOZFOO"));
     sameNormalForm(t, res);
   }
 
@@ -944,7 +944,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all)
                                    d_nodeManager->mkConst(String("ZZZ")),
                                    re,
                                    foo);
-    Node res = d_nodeManager->mkConst(::CVC5::String("ZZZ"));
+    Node res = d_nodeManager->mkConst(::cvc5::String("ZZZ"));
     sameNormalForm(t, res);
   }
 
@@ -961,7 +961,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all)
                                    d_nodeManager->mkConst(String("ZZZ")),
                                    sigStar,
                                    foo);
-    Node res = d_nodeManager->mkConst(::CVC5::String("FOOFOOFOO"));
+    Node res = d_nodeManager->mkConst(::cvc5::String("FOOFOOFOO"));
     sameNormalForm(t, res);
   }
 
@@ -978,7 +978,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_replace_all)
                                    d_nodeManager->mkConst(String("")),
                                    sigStar,
                                    foo);
-    Node res = d_nodeManager->mkConst(::CVC5::String(""));
+    Node res = d_nodeManager->mkConst(::cvc5::String(""));
     sameNormalForm(t, res);
   }
 }
@@ -988,18 +988,18 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_contains)
   TypeNode intType = d_nodeManager->integerType();
   TypeNode strType = d_nodeManager->stringType();
 
-  Node empty = d_nodeManager->mkConst(::CVC5::String(""));
-  Node a = d_nodeManager->mkConst(::CVC5::String("A"));
-  Node ab = d_nodeManager->mkConst(::CVC5::String("AB"));
-  Node b = d_nodeManager->mkConst(::CVC5::String("B"));
-  Node c = d_nodeManager->mkConst(::CVC5::String("C"));
-  Node e = d_nodeManager->mkConst(::CVC5::String("E"));
-  Node h = d_nodeManager->mkConst(::CVC5::String("H"));
-  Node j = d_nodeManager->mkConst(::CVC5::String("J"));
-  Node p = d_nodeManager->mkConst(::CVC5::String("P"));
-  Node abc = d_nodeManager->mkConst(::CVC5::String("ABC"));
-  Node def = d_nodeManager->mkConst(::CVC5::String("DEF"));
-  Node ghi = d_nodeManager->mkConst(::CVC5::String("GHI"));
+  Node empty = d_nodeManager->mkConst(::cvc5::String(""));
+  Node a = d_nodeManager->mkConst(::cvc5::String("A"));
+  Node ab = d_nodeManager->mkConst(::cvc5::String("AB"));
+  Node b = d_nodeManager->mkConst(::cvc5::String("B"));
+  Node c = d_nodeManager->mkConst(::cvc5::String("C"));
+  Node e = d_nodeManager->mkConst(::cvc5::String("E"));
+  Node h = d_nodeManager->mkConst(::cvc5::String("H"));
+  Node j = d_nodeManager->mkConst(::cvc5::String("J"));
+  Node p = d_nodeManager->mkConst(::cvc5::String("P"));
+  Node abc = d_nodeManager->mkConst(::cvc5::String("ABC"));
+  Node def = d_nodeManager->mkConst(::cvc5::String("DEF"));
+  Node ghi = d_nodeManager->mkConst(::cvc5::String("GHI"));
   Node x = d_nodeManager->mkVar("x", strType);
   Node y = d_nodeManager->mkVar("y", strType);
   Node xy = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y);
@@ -1356,9 +1356,9 @@ TEST_F(TestTheoryWhiteSequencesRewriter, infer_eqs_from_contains)
 {
   TypeNode strType = d_nodeManager->stringType();
 
-  Node empty = d_nodeManager->mkConst(::CVC5::String(""));
-  Node a = d_nodeManager->mkConst(::CVC5::String("A"));
-  Node b = d_nodeManager->mkConst(::CVC5::String("B"));
+  Node empty = d_nodeManager->mkConst(::cvc5::String(""));
+  Node a = d_nodeManager->mkConst(::cvc5::String("A"));
+  Node b = d_nodeManager->mkConst(::cvc5::String("B"));
   Node x = d_nodeManager->mkVar("x", strType);
   Node y = d_nodeManager->mkVar("y", strType);
   Node xy = d_nodeManager->mkNode(kind::STRING_CONCAT, x, y);
@@ -1400,8 +1400,8 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_prefix_suffix)
 {
   TypeNode strType = d_nodeManager->stringType();
 
-  Node empty = d_nodeManager->mkConst(::CVC5::String(""));
-  Node a = d_nodeManager->mkConst(::CVC5::String("A"));
+  Node empty = d_nodeManager->mkConst(::cvc5::String(""));
+  Node a = d_nodeManager->mkConst(::cvc5::String("A"));
   Node x = d_nodeManager->mkVar("x", strType);
   Node y = d_nodeManager->mkVar("y", strType);
   Node xx = d_nodeManager->mkNode(kind::STRING_CONCAT, x, x);
@@ -1437,11 +1437,11 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_equality_ext)
   TypeNode strType = d_nodeManager->stringType();
   TypeNode intType = d_nodeManager->integerType();
 
-  Node empty = d_nodeManager->mkConst(::CVC5::String(""));
-  Node a = d_nodeManager->mkConst(::CVC5::String("A"));
-  Node aaa = d_nodeManager->mkConst(::CVC5::String("AAA"));
-  Node b = d_nodeManager->mkConst(::CVC5::String("B"));
-  Node ba = d_nodeManager->mkConst(::CVC5::String("BA"));
+  Node empty = d_nodeManager->mkConst(::cvc5::String(""));
+  Node a = d_nodeManager->mkConst(::cvc5::String("A"));
+  Node aaa = d_nodeManager->mkConst(::cvc5::String("AAA"));
+  Node b = d_nodeManager->mkConst(::cvc5::String("B"));
+  Node ba = d_nodeManager->mkConst(::cvc5::String("BA"));
   Node w = d_nodeManager->mkVar("w", strType);
   Node x = d_nodeManager->mkVar("x", strType);
   Node y = d_nodeManager->mkVar("y", strType);
@@ -1726,14 +1726,14 @@ TEST_F(TestTheoryWhiteSequencesRewriter, strip_constant_endpoints)
   TypeNode intType = d_nodeManager->integerType();
   TypeNode strType = d_nodeManager->stringType();
 
-  Node empty = d_nodeManager->mkConst(::CVC5::String(""));
-  Node a = d_nodeManager->mkConst(::CVC5::String("A"));
-  Node ab = d_nodeManager->mkConst(::CVC5::String("AB"));
-  Node abc = d_nodeManager->mkConst(::CVC5::String("ABC"));
-  Node abcd = d_nodeManager->mkConst(::CVC5::String("ABCD"));
-  Node bc = d_nodeManager->mkConst(::CVC5::String("BC"));
-  Node c = d_nodeManager->mkConst(::CVC5::String("C"));
-  Node cd = d_nodeManager->mkConst(::CVC5::String("CD"));
+  Node empty = d_nodeManager->mkConst(::cvc5::String(""));
+  Node a = d_nodeManager->mkConst(::cvc5::String("A"));
+  Node ab = d_nodeManager->mkConst(::cvc5::String("AB"));
+  Node abc = d_nodeManager->mkConst(::cvc5::String("ABC"));
+  Node abcd = d_nodeManager->mkConst(::cvc5::String("ABCD"));
+  Node bc = d_nodeManager->mkConst(::cvc5::String("BC"));
+  Node c = d_nodeManager->mkConst(::cvc5::String("C"));
+  Node cd = d_nodeManager->mkConst(::cvc5::String("CD"));
   Node x = d_nodeManager->mkVar("x", strType);
   Node y = d_nodeManager->mkVar("y", strType);
   Node n = d_nodeManager->mkVar("n", intType);
@@ -1833,7 +1833,7 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_membership)
   TypeNode strType = d_nodeManager->stringType();
 
   std::vector<Node> vec_empty;
-  Node abc = d_nodeManager->mkConst(::CVC5::String("ABC"));
+  Node abc = d_nodeManager->mkConst(::cvc5::String("ABC"));
   Node re_abc = d_nodeManager->mkNode(kind::STRING_TO_REGEXP, abc);
   Node x = d_nodeManager->mkVar("x", strType);
 
@@ -1908,4 +1908,4 @@ TEST_F(TestTheoryWhiteSequencesRewriter, rewrite_regexp_concat)
   }
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/strings_rewriter_white.cpp b/test/unit/theory/strings_rewriter_white.cpp
index 94bf8b581..13ee14306 100644
--- a/test/unit/theory/strings_rewriter_white.cpp
+++ b/test/unit/theory/strings_rewriter_white.cpp
@@ -24,7 +24,7 @@
 #include "theory/rewriter.h"
 #include "theory/strings/strings_rewriter.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 using namespace theory;
@@ -41,8 +41,8 @@ TEST_F(TestTheoryWhiteStringsRewriter, rewrite_leq)
   TypeNode intType = d_nodeManager->integerType();
   TypeNode strType = d_nodeManager->stringType();
 
-  Node a = d_nodeManager->mkConst(::CVC5::String("A"));
-  Node bc = d_nodeManager->mkConst(::CVC5::String("BC"));
+  Node a = d_nodeManager->mkConst(::cvc5::String("A"));
+  Node bc = d_nodeManager->mkConst(::cvc5::String("BC"));
   Node x = d_nodeManager->mkVar("x", strType);
   Node y = d_nodeManager->mkVar("y", strType);
 
@@ -61,4 +61,4 @@ TEST_F(TestTheoryWhiteStringsRewriter, rewrite_leq)
 }
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp
index ac992f5c9..27ce7158a 100644
--- a/test/unit/theory/theory_arith_white.cpp
+++ b/test/unit/theory/theory_arith_white.cpp
@@ -24,7 +24,7 @@
 #include "theory/theory_engine.h"
 #include "util/rational.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace theory;
 using namespace theory::arith;
@@ -122,4 +122,4 @@ TEST_F(TestTheoryWhiteArith, int_normal_form)
   ASSERT_EQ(Rewriter::rewrite(Rewriter::rewrite(t)), Rewriter::rewrite(t));
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp
index 09f5c2ae9..88a1412a7 100644
--- a/test/unit/theory/theory_bags_normal_form_white.cpp
+++ b/test/unit/theory/theory_bags_normal_form_white.cpp
@@ -18,7 +18,7 @@
 #include "theory/bags/normal_form.h"
 #include "theory/strings/type_enumerator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace theory;
 using namespace kind;
@@ -40,7 +40,7 @@ class TestTheoryWhiteBagsNormalForm : public TestSmt
   std::vector<Node> getNStrings(size_t n)
   {
     std::vector<Node> elements(n);
-    CVC5::theory::strings::StringEnumerator enumerator(
+    cvc5::theory::strings::StringEnumerator enumerator(
         d_nodeManager->stringType());
 
     for (size_t i = 0; i < n; i++)
@@ -586,4 +586,4 @@ TEST_F(TestTheoryWhiteBagsNormalForm, to_set)
   ASSERT_EQ(output3, NormalForm::evaluate(input3));
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp
index a1cc2761a..586afd8b5 100644
--- a/test/unit/theory/theory_bags_rewriter_white.cpp
+++ b/test/unit/theory/theory_bags_rewriter_white.cpp
@@ -17,7 +17,7 @@
 #include "theory/bags/bags_rewriter.h"
 #include "theory/strings/type_enumerator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace theory;
 using namespace kind;
@@ -688,4 +688,4 @@ TEST_F(TestTheoryWhiteBagsRewriter, to_set)
               && response.d_status == REWRITE_AGAIN_FULL);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp
index 830169c8b..2948c2e9e 100644
--- a/test/unit/theory/theory_bags_type_rules_white.cpp
+++ b/test/unit/theory/theory_bags_type_rules_white.cpp
@@ -17,7 +17,7 @@
 #include "theory/bags/theory_bags_type_rules.h"
 #include "theory/strings/type_enumerator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace theory;
 using namespace kind;
@@ -33,7 +33,7 @@ class TestTheoryWhiteBagsTypeRule : public TestSmt
   std::vector<Node> getNStrings(size_t n)
   {
     std::vector<Node> elements(n);
-    CVC5::theory::strings::StringEnumerator enumerator(
+    cvc5::theory::strings::StringEnumerator enumerator(
         d_nodeManager->stringType());
 
     for (size_t i = 0; i < n; i++)
@@ -110,4 +110,4 @@ TEST_F(TestTheoryWhiteBagsTypeRule, to_set_operator)
   ASSERT_TRUE(d_nodeManager->mkNode(BAG_TO_SET, bag).getType().isSet());
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp
index ddd43a063..de3cdaf4d 100644
--- a/test/unit/theory/theory_black.cpp
+++ b/test/unit/theory/theory_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::theory
+ ** \brief Black box testing of cvc5::theory
  **
- ** Black box testing of CVC5::theory
+ ** Black box testing of cvc5::theory
  **/
 
 #include <sstream>
@@ -23,7 +23,7 @@
 #include "test_smt.h"
 #include "theory/rewriter.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 using namespace context;
@@ -129,4 +129,4 @@ TEST_F(TestTheoryBlack, array_const)
   ASSERT_TRUE(arr2.isConst());
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp
index 247f5428f..df1c3755b 100644
--- a/test/unit/theory/theory_bv_int_blaster_white.cpp
+++ b/test/unit/theory/theory_bv_int_blaster_white.cpp
@@ -22,7 +22,7 @@
 #include "theory/bv/int_blaster.h"
 #include "util/bitvector.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 using namespace theory;
@@ -44,4 +44,4 @@ class TestTheoryWhiteBvIntblaster : public TestSmtNoFinishInit
   Node d_one;
 };
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/theory_bv_rewriter_white.cpp b/test/unit/theory/theory_bv_rewriter_white.cpp
index c7262117c..e0c2dad04 100644
--- a/test/unit/theory/theory_bv_rewriter_white.cpp
+++ b/test/unit/theory/theory_bv_rewriter_white.cpp
@@ -23,7 +23,7 @@
 #include "theory/rewriter.h"
 #include "util/bitvector.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 using namespace theory;
@@ -81,4 +81,4 @@ TEST_F(TestTheoryWhiteBvRewriter, rewrite_bv_ite)
   ASSERT_EQ(nr, Rewriter::rewrite(nr));
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp
index 020c7d0a5..bcd91f9b8 100644
--- a/test/unit/theory/theory_bv_white.cpp
+++ b/test/unit/theory/theory_bv_white.cpp
@@ -25,7 +25,7 @@
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace theory;
 using namespace theory::bv;
@@ -93,4 +93,4 @@ TEST_F(TestTheoryWhiteBv, mkUmulo)
   }
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/theory_engine_white.cpp b/test/unit/theory/theory_engine_white.cpp
index ff2f3a836..57741b98d 100644
--- a/test/unit/theory/theory_engine_white.cpp
+++ b/test/unit/theory/theory_engine_white.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief White box testing of CVC5::theory::Theory.
+ ** \brief White box testing of cvc5::theory::Theory.
  **
- ** White box testing of CVC5::theory::Theory.  This test creates
+ ** White box testing of cvc5::theory::Theory.  This test creates
  ** "fake" theory interfaces and injects them into TheoryEngine, so we
  ** can test TheoryEngine's behavior without relying on independent
  ** theory behavior.  This is done in TheoryEngineWhite::setUp() by
@@ -33,7 +33,7 @@
 #include "util/integer.h"
 #include "util/rational.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace theory;
 using namespace expr;
@@ -183,4 +183,4 @@ TEST_F(TestTheoryWhiteEngine, rewrite_rules)
 }
 
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp
index fc20d6d73..6111c2640 100644
--- a/test/unit/theory/theory_int_opt_white.cpp
+++ b/test/unit/theory/theory_int_opt_white.cpp
@@ -15,7 +15,7 @@
 #include "smt/optimization_solver.h"
 #include "test_smt.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace theory;
 using namespace smt;
@@ -136,4 +136,4 @@ TEST_F(TestTheoryWhiteIntOpt, result)
   std::cout << "Result is :" << r << std::endl;
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp
index 715eea5f9..19968cbdd 100644
--- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp
+++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp
@@ -24,7 +24,7 @@
 #include "theory/rewriter.h"
 #include "util/bitvector.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace theory;
 using namespace theory::bv;
@@ -452,4 +452,4 @@ TEST_F(TestTheoryWhiteyQuantifiersBvInstantiator, normalizePvEqual)
   ASSERT_EQ(norm_axax[1], a);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
index 4ad3f04ef..64ba39e7f 100644
--- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
+++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
@@ -20,7 +20,7 @@
 #include "theory/quantifiers/bv_inverter_utils.h"
 #include "util/result.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace kind;
 using namespace theory;
@@ -1611,4 +1611,4 @@ TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_sext_sgt_false)
   runTestSext(false, BITVECTOR_SGT);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/theory_sets_type_enumerator_white.cpp b/test/unit/theory/theory_sets_type_enumerator_white.cpp
index adee0c266..f20cf50d2 100644
--- a/test/unit/theory/theory_sets_type_enumerator_white.cpp
+++ b/test/unit/theory/theory_sets_type_enumerator_white.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief White box testing of CVC5::theory::sets::SetsTypeEnumerator
+ ** \brief White box testing of cvc5::theory::sets::SetsTypeEnumerator
  **
- ** White box testing of CVC5::theory::sets::SetsTypeEnumerator.  (These tests
+ ** White box testing of cvc5::theory::sets::SetsTypeEnumerator.  (These tests
  ** depends  on the ordering that the SetsTypeEnumerator use, so it's a
  *white-box
  ** test.)
@@ -21,7 +21,7 @@
 #include "test_smt.h"
 #include "theory/sets/theory_sets_type_enumerator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace theory;
 using namespace kind;
@@ -152,4 +152,4 @@ TEST_F(TestTheoryWhiteSetsTypeEnumerator, bv)
   ASSERT_TRUE(setEnumerator.isFinished());
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/theory_sets_type_rules_white.cpp b/test/unit/theory/theory_sets_type_rules_white.cpp
index 22b0a09d6..899a75ae9 100644
--- a/test/unit/theory/theory_sets_type_rules_white.cpp
+++ b/test/unit/theory/theory_sets_type_rules_white.cpp
@@ -16,9 +16,9 @@
 #include "test_api.h"
 #include "test_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
-using namespace CVC5::api;
+using namespace cvc5::api;
 
 namespace test {
 
@@ -83,4 +83,4 @@ TEST_F(TestTheoryWhiteSetsTypeRuleInternal, singleton_node)
   ASSERT_TRUE(n.isConst());
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/theory_strings_skolem_cache_black.cpp b/test/unit/theory/theory_strings_skolem_cache_black.cpp
index 06a86b844..33543cc42 100644
--- a/test/unit/theory/theory_strings_skolem_cache_black.cpp
+++ b/test/unit/theory/theory_strings_skolem_cache_black.cpp
@@ -20,7 +20,7 @@
 #include "util/rational.h"
 #include "util/string.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace theory::strings;
 
@@ -59,4 +59,4 @@ TEST_F(TestTheoryBlackStringsSkolemCache, mkSkolemCached)
   }
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/theory_strings_word_white.cpp b/test/unit/theory/theory_strings_word_white.cpp
index 03b9ed4c2..1ea73c0cc 100644
--- a/test/unit/theory/theory_strings_word_white.cpp
+++ b/test/unit/theory/theory_strings_word_white.cpp
@@ -20,7 +20,7 @@
 #include "test_node.h"
 #include "theory/strings/word.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace theory;
 using namespace theory::strings;
@@ -121,4 +121,4 @@ TEST_F(TestTheoryWhiteStringsWord, strings)
   ASSERT_TRUE(Word::roverlap(aaaaa, aa) == 2);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/theory_white.cpp b/test/unit/theory/theory_white.cpp
index 41abdd6d1..cb6e5ebfe 100644
--- a/test/unit/theory/theory_white.cpp
+++ b/test/unit/theory/theory_white.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::theory::Theory.
+ ** \brief Black box testing of cvc5::theory::Theory.
  **
- ** Black box testing of CVC5::theory::Theory.
+ ** Black box testing of cvc5::theory::Theory.
  **/
 
 #include <memory>
@@ -24,7 +24,7 @@
 #include "theory/theory_engine.h"
 #include "util/resource_manager.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace theory;
 using namespace expr;
@@ -109,4 +109,4 @@ TEST_F(TestTheoryWhite, outputChannel)
   d_outputChannel.d_callHistory.clear();
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp
index 2e018f9cf..6cab15b27 100644
--- a/test/unit/theory/type_enumerator_white.cpp
+++ b/test/unit/theory/type_enumerator_white.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief White box testing of CVC5::theory::TypeEnumerator
+ ** \brief White box testing of cvc5::theory::TypeEnumerator
  **
- ** White box testing of CVC5::theory::TypeEnumerator.  (These tests depends
+ ** White box testing of cvc5::theory::TypeEnumerator.  (These tests depends
  ** on the ordering that the TypeEnumerators use, so it's a white-box test.)
  **/
 
@@ -25,7 +25,7 @@
 #include "test_smt.h"
 #include "theory/type_enumerator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 using namespace theory;
 using namespace kind;
@@ -332,4 +332,4 @@ TEST_F(TestTheoryWhiteTypeEnumerator, bv)
   ASSERT_THROW(*++te, NoMoreValuesException);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp
index 5be00263d..b82807835 100644
--- a/test/unit/util/array_store_all_white.cpp
+++ b/test/unit/util/array_store_all_white.cpp
@@ -9,15 +9,15 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::ArrayStoreAll
+ ** \brief Black box testing of cvc5::ArrayStoreAll
  **
- ** Black box testing of CVC5::ArrayStoreAll.
+ ** Black box testing of cvc5::ArrayStoreAll.
  **/
 
 #include "expr/array_store_all.h"
 #include "test_smt.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilWhiteArrayStoreAll : public TestSmt
@@ -75,4 +75,4 @@ TEST_F(TestUtilWhiteArrayStoreAll, const_error)
       IllegalArgumentException);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/assert_white.cpp b/test/unit/util/assert_white.cpp
index a64bf275d..bab612b62 100644
--- a/test/unit/util/assert_white.cpp
+++ b/test/unit/util/assert_white.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief White box testing of CVC5::Configuration.
+ ** \brief White box testing of cvc5::Configuration.
  **
- ** White box testing of CVC5::Configuration.
+ ** White box testing of cvc5::Configuration.
  **/
 
 #include <cstring>
@@ -20,7 +20,7 @@
 #include "base/check.h"
 #include "test.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilWhite : public TestInternal
@@ -86,4 +86,4 @@ TEST_F(TestUtilWhite, CheckArgument)
   ASSERT_THROW(CheckArgument(false, "x"), IllegalArgumentException);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/binary_heap_black.cpp b/test/unit/util/binary_heap_black.cpp
index 0b52b6d14..c00aeaeb2 100644
--- a/test/unit/util/binary_heap_black.cpp
+++ b/test/unit/util/binary_heap_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::BinaryHeap
+ ** \brief Black box testing of cvc5::BinaryHeap
  **
- ** Black box testing of CVC5::BinaryHeap.
+ ** Black box testing of cvc5::BinaryHeap.
  **/
 
 #include <iostream>
@@ -20,7 +20,7 @@
 #include "test.h"
 #include "util/bin_heap.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackBinaryHeap : public TestInternal
@@ -230,4 +230,4 @@ TEST_F(TestUtilBlackBinaryHeap, large_heap)
   ASSERT_TRUE(heap.empty());
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/bitvector_black.cpp b/test/unit/util/bitvector_black.cpp
index b26d8a1c6..61dfa8101 100644
--- a/test/unit/util/bitvector_black.cpp
+++ b/test/unit/util/bitvector_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::BitVector
+ ** \brief Black box testing of cvc5::BitVector
  **
- ** Black box testing of CVC5::BitVector.
+ ** Black box testing of cvc5::BitVector.
  **/
 
 #include <sstream>
@@ -19,7 +19,7 @@
 #include "test.h"
 #include "util/bitvector.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackBitVector : public TestInternal
@@ -203,4 +203,4 @@ TEST_F(TestUtilBlackBitVector, static_helpers)
   ASSERT_EQ(BitVector::mkMaxSigned(4).toSignedInteger(), Integer(7));
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp
index cce2518c4..baacbce5a 100644
--- a/test/unit/util/boolean_simplification_black.cpp
+++ b/test/unit/util/boolean_simplification_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::BooleanSimplification
+ ** \brief Black box testing of cvc5::BooleanSimplification
  **
- ** Black box testing of CVC5::BooleanSimplification.
+ ** Black box testing of cvc5::BooleanSimplification.
  **/
 
 #include <algorithm>
@@ -26,7 +26,7 @@
 #include "smt_util/boolean_simplification.h"
 #include "test_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackBooleanSimplification : public TestNode
@@ -248,4 +248,4 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyConflict)
 #endif
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/cardinality_black.cpp b/test/unit/util/cardinality_black.cpp
index b4b6ab6a5..f4b2f3ac4 100644
--- a/test/unit/util/cardinality_black.cpp
+++ b/test/unit/util/cardinality_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Public-box testing of CVC5::Cardinality
+ ** \brief Public-box testing of cvc5::Cardinality
  **
- ** Public-box testing of CVC5::Cardinality.
+ ** Public-box testing of cvc5::Cardinality.
  **/
 
 #include <sstream>
@@ -22,7 +22,7 @@
 #include "util/cardinality.h"
 #include "util/integer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackCardinality : public TestInternal
@@ -270,4 +270,4 @@ TEST_F(TestUtilBlackCardinality, cardinalities)
   ASSERT_EQ((z ^ z).getBethNumber(), 3);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/check_white.cpp b/test/unit/util/check_white.cpp
index 4985bced3..4909e3a58 100644
--- a/test/unit/util/check_white.cpp
+++ b/test/unit/util/check_white.cpp
@@ -20,7 +20,7 @@
 #include "base/check.h"
 #include "test.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilWhiteCheck : public TestInternal
@@ -63,4 +63,4 @@ TEST_F(TestUtilWhiteCheck, expect_abort)
   ASSERT_DEATH(AlwaysAssert(false), "false");
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/configuration_black.cpp b/test/unit/util/configuration_black.cpp
index a7c5c2703..35bfd4d78 100644
--- a/test/unit/util/configuration_black.cpp
+++ b/test/unit/util/configuration_black.cpp
@@ -9,15 +9,15 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::Configuration.
+ ** \brief Black box testing of cvc5::Configuration.
  **
- ** Black box testing of CVC5::Configuration.
+ ** Black box testing of cvc5::Configuration.
  **/
 
 #include "base/configuration.h"
 #include "test.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackConfiguration : public TestInternal
@@ -96,4 +96,4 @@ TEST_F(TestUtilBlackConfiguration, about)
   Configuration::about();
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp
index b486d91e9..37cfe0cfa 100644
--- a/test/unit/util/datatype_black.cpp
+++ b/test/unit/util/datatype_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::DType
+ ** \brief Black box testing of cvc5::DType
  **
- ** Black box testing of CVC5::DType.
+ ** Black box testing of cvc5::DType.
  **/
 
 #include <sstream>
@@ -21,7 +21,7 @@
 #include "expr/type_node.h"
 #include "test_smt.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackDatatype : public TestSmt
@@ -495,4 +495,4 @@ TEST_F(TestUtilBlackDatatype, parametric_DType)
   ASSERT_EQ(TypeNode::leastCommonTypeNode(pairIntInt, pairIntInt), pairIntInt);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/exception_black.cpp b/test/unit/util/exception_black.cpp
index 7216c0b8c..2884dbfb8 100644
--- a/test/unit/util/exception_black.cpp
+++ b/test/unit/util/exception_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::Exception.
+ ** \brief Black box testing of cvc5::Exception.
  **
- ** Black box testing of CVC5::Exception.
+ ** Black box testing of cvc5::Exception.
  **/
 
 #include <iostream>
@@ -20,14 +20,14 @@
 #include "base/exception.h"
 #include "test.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackException : public TestInternal
 {
 };
 
-// CVC5::Exception is a simple class, just test it all at once.
+// cvc5::Exception is a simple class, just test it all at once.
 TEST_F(TestUtilBlackException, exceptions)
 {
   Exception e1;
@@ -52,4 +52,4 @@ TEST_F(TestUtilBlackException, exceptions)
   ASSERT_EQ(s3.str(), std::string("three of 'em!"));
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/floatingpoint_black.cpp b/test/unit/util/floatingpoint_black.cpp
index 391c656f3..0fe48928f 100644
--- a/test/unit/util/floatingpoint_black.cpp
+++ b/test/unit/util/floatingpoint_black.cpp
@@ -9,15 +9,15 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::FloatingPoint.
+ ** \brief Black box testing of cvc5::FloatingPoint.
  **
- ** Black box testing of CVC5::FloatingPoint.
+ ** Black box testing of cvc5::FloatingPoint.
  **/
 
 #include "test.h"
 #include "util/floatingpoint.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackFloatingPoint : public TestInternal
@@ -136,4 +136,4 @@ TEST_F(TestUtilBlackFloatingPoint, makeMaxNormal)
   ASSERT_TRUE(mfp128.isNormal());
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/integer_black.cpp b/test/unit/util/integer_black.cpp
index fc92fa0d2..1a3e75256 100644
--- a/test/unit/util/integer_black.cpp
+++ b/test/unit/util/integer_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::Integer.
+ ** \brief Black box testing of cvc5::Integer.
  **
- ** Black box testing of CVC5::Integer.
+ ** Black box testing of cvc5::Integer.
  **/
 
 #include <limits>
@@ -21,7 +21,7 @@
 #include "test.h"
 #include "util/integer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackInteger : public TestInternal
@@ -564,4 +564,4 @@ TEST_F(TestUtilBlackInteger, modInverse)
   }
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/integer_white.cpp b/test/unit/util/integer_white.cpp
index 3b5363dda..117f82195 100644
--- a/test/unit/util/integer_white.cpp
+++ b/test/unit/util/integer_white.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief White box testing of CVC5::Integer.
+ ** \brief White box testing of cvc5::Integer.
  **
- ** White box testing of CVC5::Integer.
+ ** White box testing of cvc5::Integer.
  **/
 
 #include <sstream>
@@ -19,7 +19,7 @@
 #include "test.h"
 #include "util/integer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilWhiteInteger : public TestInternal
@@ -53,4 +53,4 @@ TEST_F(TestUtilWhiteInteger, construction)
   ASSERT_EQ(Integer(u), Integer(u));
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/output_black.cpp b/test/unit/util/output_black.cpp
index f5c973849..e951dd114 100644
--- a/test/unit/util/output_black.cpp
+++ b/test/unit/util/output_black.cpp
@@ -20,7 +20,7 @@
 #include "base/output.h"
 #include "test.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackOutput : public TestInternal
@@ -241,4 +241,4 @@ TEST_F(TestUtilBlackOutput, simple_print)
 #endif /* CVC4_MUZZLE */
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/rational_black.cpp b/test/unit/util/rational_black.cpp
index e6dee5d55..d3b116d26 100644
--- a/test/unit/util/rational_black.cpp
+++ b/test/unit/util/rational_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::Rational.
+ ** \brief Black box testing of cvc5::Rational.
  **
- ** Black box testing of CVC5::Rational.
+ ** Black box testing of cvc5::Rational.
  **/
 
 #include <sstream>
@@ -19,7 +19,7 @@
 #include "test.h"
 #include "util/rational.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackRational : public TestInternal
@@ -44,4 +44,4 @@ TEST_F(TestUtilBlackRational, fromDecimal)
   ASSERT_THROW(Rational::fromDecimal("Hello, world!");, std::invalid_argument);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/rational_white.cpp b/test/unit/util/rational_white.cpp
index 542a43990..c5b52e3c8 100644
--- a/test/unit/util/rational_white.cpp
+++ b/test/unit/util/rational_white.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief White box testing of CVC5::Rational.
+ ** \brief White box testing of cvc5::Rational.
  **
- ** White box testing of CVC5::Rational.
+ ** White box testing of cvc5::Rational.
  **/
 
 #include <sstream>
@@ -19,7 +19,7 @@
 #include "test.h"
 #include "util/rational.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilWhiteRational : public TestInternal
@@ -416,4 +416,4 @@ TEST_F(TestUtilWhiteRational, constructrion)
   ASSERT_EQ(Rational(u), Rational(u));
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/real_algebraic_number_black.cpp b/test/unit/util/real_algebraic_number_black.cpp
index 4300b709c..507be5ea0 100644
--- a/test/unit/util/real_algebraic_number_black.cpp
+++ b/test/unit/util/real_algebraic_number_black.cpp
@@ -9,15 +9,15 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::RealAlgebraicNumber.
+ ** \brief Black box testing of cvc5::RealAlgebraicNumber.
  **
- ** Black box testing of CVC5::RealAlgebraicNumber.
+ ** Black box testing of cvc5::RealAlgebraicNumber.
  **/
 
 #include "test.h"
 #include "util/real_algebraic_number.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 #ifndef CVC4_POLY_IMP
@@ -81,4 +81,4 @@ TEST_F(TestUtilBlackRealAlgebraicNumber, arithmetic)
   ASSERT_EQ(msqrt2 * sqrt2, RealAlgebraicNumber(Integer(-2)));
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/stats_black.cpp b/test/unit/util/stats_black.cpp
index f8a14d9b2..2ee64ab33 100644
--- a/test/unit/util/stats_black.cpp
+++ b/test/unit/util/stats_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC5::Stat and associated classes
+ ** \brief Black box testing of cvc5::Stat and associated classes
  **
- ** Black box testing of CVC5::Stat and associated classes.
+ ** Black box testing of cvc5::Stat and associated classes.
  **/
 
 #include <fcntl.h>
@@ -27,7 +27,7 @@
 #include "util/stats_histogram.h"
 #include "util/stats_timer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackStats : public TestInternal
@@ -49,7 +49,7 @@ TEST_F(TestUtilBlackStats, stats)
   BackedStat<void*> backedAddr("backedDouble", (void*)0xDEADBEEF);
   IntegralHistogramStat<std::int64_t> histIntStat("hist-int");
   histIntStat << 15 << 16 << 15 << 14 << 16;
-  IntegralHistogramStat<CVC5::PfRule> histPfRuleStat("hist-pfrule");
+  IntegralHistogramStat<cvc5::PfRule> histPfRuleStat("hist-pfrule");
   histPfRuleStat << PfRule::ASSUME << PfRule::SCOPE << PfRule::ASSUME;
 
   // A statistic with no safe_print support
@@ -161,4 +161,4 @@ TEST_F(TestUtilBlackStats, stats)
 #endif
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5