Rename namespace CVC5 to cvc5. (#6258)

57 files changed, 218 insertions, 218 deletions

diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index ee4b467b8..62c458723 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -23,13 +23,13 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5;
-using namespace CVC5::theory;
-using namespace CVC5::theory::bv;
-using namespace CVC5::context;
+using namespace cvc5;
+using namespace cvc5::theory;
+using namespace cvc5::theory::bv;
+using namespace cvc5::context;
 
 using namespace std;
-using namespace CVC5::theory::bv::utils;
+using namespace cvc5::theory::bv::utils;
 
 bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions,
                                          std::vector<Node>& new_assertions)
diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h
index 6c36de34c..182b29c19 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -27,7 +27,7 @@
 #include "util/statistics_registry.h"
 #include "util/stats_timer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -246,6 +246,6 @@ public:
 
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index 002a4f631..fb5adb54c 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.cpp
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -40,7 +40,7 @@ static inline int Cnf_Lit2Var(int Lit)
   return (Lit & 1) ? -(Lit >> 1) - 1 : (Lit >> 1) + 1;
 }
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -123,7 +123,7 @@ Abc_Ntk_t* AigBitblaster::currentAigNtk() {
   if (!AigBitblaster::s_abcAigNetwork) {
     Abc_Start();
     s_abcAigNetwork = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1);
-    char pName[] = "CVC5::theory::bv::AigNetwork";
+    char pName[] = "cvc5::theory::bv::AigNetwork";
     s_abcAigNetwork->pName = Extra_UtilStrsav(pName);
   }
   
@@ -496,5 +496,5 @@ AigBitblaster::Statistics::~Statistics() {
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 #endif // CVC4_USE_ABC
diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
index 3eccbd3ec..002ca71ec 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -33,7 +33,7 @@ typedef Abc_Aig_t_ Abc_Aig_t;
 class Cnf_Dat_t_;
 typedef Cnf_Dat_t_ Cnf_Dat_t;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 class SatSolver;
 }
@@ -121,6 +121,6 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*>
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif  //  CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h
index 7ae55015f..72b079321 100644
--- a/src/theory/bv/bitblast/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast/bitblast_strategies_template.h
@@ -27,7 +27,7 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 namespace theory {
 namespace bv {
@@ -899,6 +899,6 @@ void DefaultRotateLeftBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb)
 
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/bv/bitblast/bitblast_utils.h b/src/theory/bv/bitblast/bitblast_utils.h
index e342d4410..461d7fcaf 100644
--- a/src/theory/bv/bitblast/bitblast_utils.h
+++ b/src/theory/bv/bitblast/bitblast_utils.h
@@ -23,7 +23,7 @@
 #include <ostream>
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -267,6 +267,6 @@ T inline sLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqu
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif  // CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index 90ea5ac2b..311d44c94 100644
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -35,7 +35,7 @@
 #include "theory/valuation.h"
 #include "util/resource_manager.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -268,6 +268,6 @@ Node TBitblaster<T>::getTermModel(TNode node, bool fullModel)
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BV__BITBLAST__BITBLASTER_H */
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 5e22262e2..41fadd8b0 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -27,7 +27,7 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/theory_model.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -288,4 +288,4 @@ bool EagerBitblaster::isSharedTerm(TNode node) {
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index dead462b5..87699df40 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -26,7 +26,7 @@
 
 #include "prop/sat_solver.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -85,5 +85,5 @@ class BitblastingRegistrar : public prop::Registrar
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 #endif  //  CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index e20a6f6b5..a5d3e9bb6 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -30,7 +30,7 @@
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -590,4 +590,4 @@ void TLazyBitblaster::clearSolver() {
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index 1a963e67d..91995b56b 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -26,7 +26,7 @@
 #include "prop/bv_sat_solver_notify.h"
 #include "theory/bv/abstraction.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 class CnfStream;
 class NullRegistrat;
@@ -176,5 +176,5 @@ class TLazyBitblaster : public TBitblaster<Node>
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 #endif  //  CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp
index b0cf68609..a441e769e 100644
--- a/src/theory/bv/bitblast/proof_bitblaster.cpp
+++ b/src/theory/bv/bitblast/proof_bitblaster.cpp
@@ -17,7 +17,7 @@
 
 #include "theory/theory_model.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -84,4 +84,4 @@ bool BBProof::collectModelValues(TheoryModel* m,
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h
index 894a9a916..4983b485e 100644
--- a/src/theory/bv/bitblast/proof_bitblaster.h
+++ b/src/theory/bv/bitblast/proof_bitblaster.h
@@ -18,7 +18,7 @@
 
 #include "theory/bv/bitblast/simple_bitblaster.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -47,5 +47,5 @@ class BBProof
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 #endif
diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp
index 76677e2db..05227ed09 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.cpp
+++ b/src/theory/bv/bitblast/simple_bitblaster.cpp
@@ -17,7 +17,7 @@
 #include "theory/theory_model.h"
 #include "theory/theory_state.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -155,4 +155,4 @@ bool BBSimple::isVariable(TNode node)
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h
index 1b48f9a68..300b93b53 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.h
+++ b/src/theory/bv/bitblast/simple_bitblaster.h
@@ -19,7 +19,7 @@
 
 #include "theory/bv/bitblast/bitblaster.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -75,6 +75,6 @@ class BBSimple : public TBitblaster<Node>
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 9c478791c..97df17c58 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -23,7 +23,7 @@
 
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -125,4 +125,4 @@ bool EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel)
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 0fe1ed32b..17e6c50e7 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -23,7 +23,7 @@
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/theory_model.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -60,6 +60,6 @@ class EagerBitblastSolver {
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif  // CVC4__THEORY__BV__BV_EAGER_SOLVER_H
diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index 67554525a..27063ea7a 100644
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -18,15 +18,15 @@
 #include "theory/bv/theory_bv_utils.h"
 
 using namespace std;
-using namespace CVC5;
-using namespace CVC5::context;
-using namespace CVC5::theory;
-using namespace CVC5::theory::bv;
-using namespace CVC5::theory::bv::utils;
-
-const TermId CVC5::theory::bv::UndefinedTermId = -1;
-const ReasonId CVC5::theory::bv::UndefinedReasonId = -1;
-const ReasonId CVC5::theory::bv::AxiomReasonId = -2;
+using namespace cvc5;
+using namespace cvc5::context;
+using namespace cvc5::theory;
+using namespace cvc5::theory::bv;
+using namespace cvc5::theory::bv::utils;
+
+const TermId cvc5::theory::bv::UndefinedTermId = -1;
+const ReasonId cvc5::theory::bv::UndefinedReasonId = -1;
+const ReasonId cvc5::theory::bv::AxiomReasonId = -2;
 
 bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) {
   Debug("bv-inequality") << "InequalityGraph::addInequality " << a << " " << b << " strict: " << strict << "\n"; 
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index caa7220cf..3e856b789 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -29,7 +29,7 @@
 #include "context/cdqueue.h"
 #include "context/context.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -291,6 +291,6 @@ public:
 
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H */
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index bbb2f1ca9..983a61eb5 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -21,9 +21,9 @@
 #include "theory/bv/bv_solver_lazy.h"
 #include "theory/bv/theory_bv_utils.h"
 
-using namespace CVC5::prop;
+using namespace cvc5::prop;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -381,4 +381,4 @@ QuickXPlain::Statistics::~Statistics() {
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index 3d30d912d..7dbd01dcd 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -29,7 +29,7 @@
 #include "util/statistics_registry.h"
 #include "util/stats_timer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 class TheoryModel;
@@ -181,6 +181,6 @@ class QuickXPlain
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__BV_QUICK_CHECK_H */
diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h
index f08f7527a..faa285b97 100644
--- a/src/theory/bv/bv_solver.h
+++ b/src/theory/bv/bv_solver.h
@@ -21,7 +21,7 @@
 
 #include "theory/theory.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -117,6 +117,6 @@ class BVSolver
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BV__BV_SOLVER_H */
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index 16a99c2e4..125cb243f 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -23,7 +23,7 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -281,4 +281,4 @@ Node BVSolverBitblast::getValue(TNode node)
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h
index 794b9fa9b..86a75e0aa 100644
--- a/src/theory/bv/bv_solver_bitblast.h
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -29,7 +29,7 @@
 #include "theory/bv/proof_checker.h"
 #include "theory/eager_proof_generator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 namespace theory {
 namespace bv {
@@ -143,6 +143,6 @@ class BVSolverBitblast : public BVSolver
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index ed71fccbe..00190233c 100644
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -32,9 +32,9 @@
 #include "theory/theory_model.h"
 #include "theory/trust_substitutions.h"
 
-using namespace CVC5::theory::bv::utils;
+using namespace cvc5::theory::bv::utils;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -828,4 +828,4 @@ void BVSolverLazy::setConflict(Node conflict)
 
 }  // namespace bv
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h
index 6511900eb..ea647346e 100644
--- a/src/theory/bv/bv_solver_lazy.h
+++ b/src/theory/bv/bv_solver_lazy.h
@@ -28,7 +28,7 @@
 #include "theory/bv/theory_bv.h"
 #include "util/hash.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -229,6 +229,6 @@ class BVSolverLazy : public BVSolver
 }  // namespace bv
 }  // namespace theory
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BV__BV_SOLVER_LAZY_H */
diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp
index 65d46e861..c96e8d0bc 100644
--- a/src/theory/bv/bv_solver_simple.cpp
+++ b/src/theory/bv/bv_solver_simple.cpp
@@ -20,7 +20,7 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -151,4 +151,4 @@ bool BVSolverSimple::collectModelValues(TheoryModel* m,
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h
index 1b6976abb..8983bddb2 100644
--- a/src/theory/bv/bv_solver_simple.h
+++ b/src/theory/bv/bv_solver_simple.h
@@ -24,7 +24,7 @@
 #include "theory/bv/proof_checker.h"
 #include "theory/eager_proof_generator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 namespace theory {
 namespace bv {
@@ -81,6 +81,6 @@ class BVSolverSimple : public BVSolver
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index e558ea7c7..dec4614d3 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -23,7 +23,7 @@
 #include "theory/uf/equality_engine.h"
 #include "theory/theory.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 namespace theory {
 
@@ -107,6 +107,6 @@ class SubtheorySolver {
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BV__BV_SUBTHEORY_H */
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 2343d72d1..c025dab5d 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -31,12 +31,12 @@
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
-using namespace CVC5::context;
-using namespace CVC5::prop;
-using namespace CVC5::theory::bv::utils;
+using namespace cvc5::context;
+using namespace cvc5::prop;
+using namespace cvc5::theory::bv::utils;
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -992,4 +992,4 @@ Node mergeExplanations(TNode expl1, TNode expl2) {
 
 }  // namespace bv
 } /* namespace CVc4::theory */
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index e7156a33e..01209331f 100644
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -25,7 +25,7 @@
 #include "theory/bv/slicer.h"
 #include "theory/substitutions.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -245,4 +245,4 @@ class AlgebraicSolver : public SubtheorySolver
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 2d21a8f0c..f67f11e42 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -27,9 +27,9 @@
 #include "theory/bv/theory_bv_utils.h"
 
 using namespace std;
-using namespace CVC5::context;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -278,4 +278,4 @@ void BitblastSolver::setConflict(TNode conflict)
 
 }  // namespace bv
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index f964fb995..2a6930184 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -22,7 +22,7 @@
 
 #include "theory/bv/bv_subtheory.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 namespace theory {
 namespace bv {
@@ -83,4 +83,4 @@ class BitblastSolver : public SubtheorySolver
 
 }  // namespace bv
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 486adfdb7..4f89eff71 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -25,11 +25,11 @@
 #include "theory/theory_model.h"
 
 using namespace std;
-using namespace CVC5;
-using namespace CVC5::context;
-using namespace CVC5::theory;
-using namespace CVC5::theory::bv;
-using namespace CVC5::theory::bv::utils;
+using namespace cvc5;
+using namespace cvc5::context;
+using namespace cvc5::theory;
+using namespace cvc5::theory::bv;
+using namespace cvc5::theory::bv::utils;
 
 bool CoreSolverExtTheoryCallback::getCurrentSubstitution(
     int effort,
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 700d8c4f5..042f2e73c 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -25,7 +25,7 @@
 #include "theory/bv/bv_subtheory.h"
 #include "theory/ext_theory.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -164,4 +164,4 @@ class CoreSolver : public SubtheorySolver {
 
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index d67a5c550..c95d5e2dd 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -24,11 +24,11 @@
 #include "theory/theory_model.h"
 
 using namespace std;
-using namespace CVC5;
-using namespace CVC5::context;
-using namespace CVC5::theory;
-using namespace CVC5::theory::bv;
-using namespace CVC5::theory::bv::utils;
+using namespace cvc5;
+using namespace cvc5::context;
+using namespace cvc5::theory;
+using namespace cvc5::theory::bv;
+using namespace cvc5::theory::bv::utils;
 
 bool InequalitySolver::check(Theory::Effort e) {
   Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 232c8676e..dc585b49b 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -26,7 +26,7 @@
 #include "theory/bv/bv_inequality_graph.h"
 #include "theory/bv/bv_subtheory.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -89,6 +89,6 @@ class InequalitySolver : public SubtheorySolver
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */
diff --git a/src/theory/bv/int_blaster.h b/src/theory/bv/int_blaster.h
index 65a8b5480..b76fc1cb7 100644
--- a/src/theory/bv/int_blaster.h
+++ b/src/theory/bv/int_blaster.h
@@ -24,7 +24,7 @@
 #include "options/smt_options.h"
 #include "theory/arith/nl/iand_utils.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 /*
 ** Converts bit-vector formulas to integer formulas.
@@ -349,6 +349,6 @@ class IntBlaster
   bool d_introduceFreshIntVars;
 };
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* __CVC4__THEORY__BV__INT_BLASTER_H */
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 884ee49e6..3a1032bc3 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -4,36 +4,36 @@
 # src/theory/builtin/kinds.
 #
 
-theory THEORY_BV ::CVC5::theory::bv::TheoryBV "theory/bv/theory_bv.h"
+theory THEORY_BV ::cvc5::theory::bv::TheoryBV "theory/bv/theory_bv.h"
 typechecker "theory/bv/theory_bv_type_rules.h"
 
 properties finite
 properties check propagate presolve ppStaticLearn
 
-rewriter ::CVC5::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
+rewriter ::cvc5::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
 
 constant BITVECTOR_TYPE \
-	::CVC5::BitVectorSize \
-	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorSize >" \
+	::cvc5::BitVectorSize \
+	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSize >" \
 	"util/bitvector.h" \
 	"bit-vector type"
 cardinality BITVECTOR_TYPE \
-	"::CVC5::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \
+	"::cvc5::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \
 	"theory/bv/theory_bv_type_rules.h"
 
 constant CONST_BITVECTOR \
-    ::CVC5::BitVector \
-    ::CVC5::BitVectorHashFunction \
+    ::cvc5::BitVector \
+    ::cvc5::BitVectorHashFunction \
     "util/bitvector.h" \
-    "a fixed-width bit-vector constant; payload is an instance of the CVC5::BitVector class"
+    "a fixed-width bit-vector constant; payload is an instance of the cvc5::BitVector class"
 
 enumerator BITVECTOR_TYPE \
-    "::CVC5::theory::bv::BitVectorEnumerator" \
+    "::cvc5::theory::bv::BitVectorEnumerator" \
     "theory/bv/type_enumerator.h"
 
 well-founded BITVECTOR_TYPE \
     true \
-    "(*CVC5::theory::TypeEnumerator(%TYPE%))" \
+    "(*cvc5::theory::TypeEnumerator(%TYPE%))" \
     "theory/type_enumerator.h"
 
 ### non-parameterized operator kinds ------------------------------------------
@@ -99,139 +99,139 @@ operator BITVECTOR_EAGER_ATOM 1 "formula to be treated as a bv atom via eager bi
 ### parameterized operator kinds ----------------------------------------------
 
 constant BITVECTOR_BITOF_OP \
-	::CVC5::BitVectorBitOf \
-	::CVC5::BitVectorBitOfHashFunction \
+	::cvc5::BitVectorBitOf \
+	::cvc5::BitVectorBitOfHashFunction \
 	"util/bitvector.h" \
-	"operator for the bit-vector boolean bit extract; payload is an instance of the CVC5::BitVectorBitOf class"
+	"operator for the bit-vector boolean bit extract; payload is an instance of the cvc5::BitVectorBitOf class"
 parameterized BITVECTOR_BITOF BITVECTOR_BITOF_OP 1 "bit-vector boolean bit extract; first parameter is a BITVECTOR_BITOF_OP, second is a bit-vector term"
 
 constant BITVECTOR_EXTRACT_OP \
-	::CVC5::BitVectorExtract \
-	::CVC5::BitVectorExtractHashFunction \
+	::cvc5::BitVectorExtract \
+	::cvc5::BitVectorExtractHashFunction \
 	"util/bitvector.h" \
-	"operator for the bit-vector extract; payload is an instance of the CVC5::BitVectorExtract class"
+	"operator for the bit-vector extract; payload is an instance of the cvc5::BitVectorExtract class"
 parameterized BITVECTOR_EXTRACT BITVECTOR_EXTRACT_OP 1 "bit-vector extract; first parameter is a BITVECTOR_EXTRACT_OP, second is a bit-vector term"
 
 constant BITVECTOR_REPEAT_OP \
-	::CVC5::BitVectorRepeat \
-	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorRepeat >" \
+	::cvc5::BitVectorRepeat \
+	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRepeat >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector repeat; payload is an instance of the CVC5::BitVectorRepeat class"
+	"operator for the bit-vector repeat; payload is an instance of the cvc5::BitVectorRepeat class"
 parameterized BITVECTOR_REPEAT BITVECTOR_REPEAT_OP 1 "bit-vector repeat; first parameter is a BITVECTOR_REPEAT_OP, second is a bit-vector term"
 
 constant BITVECTOR_ROTATE_LEFT_OP \
-	::CVC5::BitVectorRotateLeft \
-	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorRotateLeft >" \
+	::cvc5::BitVectorRotateLeft \
+	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateLeft >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector rotate left; payload is an instance of the CVC5::BitVectorRotateLeft class"
+	"operator for the bit-vector rotate left; payload is an instance of the cvc5::BitVectorRotateLeft class"
 parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left; first parameter is a BITVECTOR_ROTATE_LEFT_OP, second is a bit-vector term"
 
 constant BITVECTOR_ROTATE_RIGHT_OP \
-	::CVC5::BitVectorRotateRight \
-	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorRotateRight >" \
+	::cvc5::BitVectorRotateRight \
+	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorRotateRight >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector rotate right; payload is an instance of the CVC5::BitVectorRotateRight class"
+	"operator for the bit-vector rotate right; payload is an instance of the cvc5::BitVectorRotateRight class"
 parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right; first parameter is a BITVECTOR_ROTATE_RIGHT_OP, second is a bit-vector term"
 
 constant BITVECTOR_SIGN_EXTEND_OP \
-	::CVC5::BitVectorSignExtend \
-	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorSignExtend >" \
+	::cvc5::BitVectorSignExtend \
+	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorSignExtend >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector sign-extend; payload is an instance of the CVC5::BitVectorSignExtend class"
+	"operator for the bit-vector sign-extend; payload is an instance of the cvc5::BitVectorSignExtend class"
 parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign-extend; first parameter is a BITVECTOR_SIGN_EXTEND_OP, second is a bit-vector term"
 
 constant BITVECTOR_ZERO_EXTEND_OP \
-	::CVC5::BitVectorZeroExtend \
-	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorZeroExtend >" \
+	::cvc5::BitVectorZeroExtend \
+	"::cvc5::UnsignedHashFunction< ::cvc5::BitVectorZeroExtend >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector zero-extend; payload is an instance of the CVC5::BitVectorZeroExtend class"
+	"operator for the bit-vector zero-extend; payload is an instance of the cvc5::BitVectorZeroExtend class"
 parameterized BITVECTOR_ZERO_EXTEND BITVECTOR_ZERO_EXTEND_OP 1 "bit-vector zero-extend; first parameter is a BITVECTOR_ZERO_EXTEND_OP, second is a bit-vector term"
 
 constant INT_TO_BITVECTOR_OP \
-	::CVC5::IntToBitVector \
-	"::CVC5::UnsignedHashFunction< ::CVC5::IntToBitVector >" \
+	::cvc5::IntToBitVector \
+	"::cvc5::UnsignedHashFunction< ::cvc5::IntToBitVector >" \
 	"util/bitvector.h" \
-	"operator for the integer conversion to bit-vector; payload is an instance of the CVC5::IntToBitVector class"
+	"operator for the integer conversion to bit-vector; payload is an instance of the cvc5::IntToBitVector class"
 parameterized INT_TO_BITVECTOR INT_TO_BITVECTOR_OP 1 "integer conversion to bit-vector; first parameter is an INT_TO_BITVECTOR_OP, second is an integer term"
 
 ### type rules for non-parameterized operator kinds ---------------------------
 
-typerule CONST_BITVECTOR ::CVC5::theory::bv::BitVectorConstantTypeRule
+typerule CONST_BITVECTOR ::cvc5::theory::bv::BitVectorConstantTypeRule
 
 ## concatentation kind
-typerule BITVECTOR_CONCAT ::CVC5::theory::bv::BitVectorConcatTypeRule
+typerule BITVECTOR_CONCAT ::cvc5::theory::bv::BitVectorConcatTypeRule
 
 ## bit-wise kinds
-typerule BITVECTOR_AND ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_COMP ::CVC5::theory::bv::BitVectorBVPredTypeRule
-typerule BITVECTOR_NAND ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_NOR ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_NOT ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_OR ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_XNOR ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_XOR ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_AND ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_COMP ::cvc5::theory::bv::BitVectorBVPredTypeRule
+typerule BITVECTOR_NAND ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_NOR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_NOT ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_OR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_XNOR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_XOR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
 
 ## arithmetic kinds
-typerule BITVECTOR_MULT ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_NEG ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_PLUS ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SUB ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_UDIV ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_UREM ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SDIV ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SMOD ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SREM ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_MULT ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_NEG ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_PLUS ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SUB ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_UDIV ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_UREM ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SDIV ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SMOD ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SREM ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
 
 ## shift kinds
-typerule BITVECTOR_ASHR ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_LSHR ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SHL ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_ASHR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_LSHR ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_SHL ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
 
 ## inequality kinds
-typerule BITVECTOR_ULE ::CVC5::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_ULT ::CVC5::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_UGE ::CVC5::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_UGT ::CVC5::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_SLE ::CVC5::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_SLT ::CVC5::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_SGE ::CVC5::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_SGT ::CVC5::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_ULE ::cvc5::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_ULT ::cvc5::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_UGE ::cvc5::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_UGT ::cvc5::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_SLE ::cvc5::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_SLT ::cvc5::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_SGE ::cvc5::theory::bv::BitVectorPredicateTypeRule
+typerule BITVECTOR_SGT ::cvc5::theory::bv::BitVectorPredicateTypeRule
 # inequalities with return type bit-vector of size 1
-typerule BITVECTOR_ULTBV ::CVC5::theory::bv::BitVectorBVPredTypeRule
-typerule BITVECTOR_SLTBV ::CVC5::theory::bv::BitVectorBVPredTypeRule
+typerule BITVECTOR_ULTBV ::cvc5::theory::bv::BitVectorBVPredTypeRule
+typerule BITVECTOR_SLTBV ::cvc5::theory::bv::BitVectorBVPredTypeRule
 
 ## if-then-else kind
-typerule BITVECTOR_ITE ::CVC5::theory::bv::BitVectorITETypeRule
+typerule BITVECTOR_ITE ::cvc5::theory::bv::BitVectorITETypeRule
 
 ## reduction kinds
-typerule BITVECTOR_REDAND ::CVC5::theory::bv::BitVectorUnaryPredicateTypeRule
-typerule BITVECTOR_REDOR ::CVC5::theory::bv::BitVectorUnaryPredicateTypeRule
+typerule BITVECTOR_REDAND ::cvc5::theory::bv::BitVectorUnaryPredicateTypeRule
+typerule BITVECTOR_REDOR ::cvc5::theory::bv::BitVectorUnaryPredicateTypeRule
 
 ## conversion kinds
-typerule BITVECTOR_TO_NAT ::CVC5::theory::bv::BitVectorConversionTypeRule
+typerule BITVECTOR_TO_NAT ::cvc5::theory::bv::BitVectorConversionTypeRule
 
 ## internal kinds
-typerule BITVECTOR_ACKERMANNIZE_UDIV ::CVC5::theory::bv::BitVectorAckermanizationUdivTypeRule
-typerule BITVECTOR_ACKERMANNIZE_UREM ::CVC5::theory::bv::BitVectorAckermanizationUremTypeRule
-typerule BITVECTOR_EAGER_ATOM ::CVC5::theory::bv::BitVectorEagerAtomTypeRule
+typerule BITVECTOR_ACKERMANNIZE_UDIV ::cvc5::theory::bv::BitVectorAckermanizationUdivTypeRule
+typerule BITVECTOR_ACKERMANNIZE_UREM ::cvc5::theory::bv::BitVectorAckermanizationUremTypeRule
+typerule BITVECTOR_EAGER_ATOM ::cvc5::theory::bv::BitVectorEagerAtomTypeRule
 
 ### type rules for parameterized operator kinds -------------------------------
 
 typerule BITVECTOR_BITOF_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_BITOF ::CVC5::theory::bv::BitVectorBitOfTypeRule
+typerule BITVECTOR_BITOF ::cvc5::theory::bv::BitVectorBitOfTypeRule
 typerule BITVECTOR_EXTRACT_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_EXTRACT ::CVC5::theory::bv::BitVectorExtractTypeRule
+typerule BITVECTOR_EXTRACT ::cvc5::theory::bv::BitVectorExtractTypeRule
 typerule BITVECTOR_REPEAT_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_REPEAT ::CVC5::theory::bv::BitVectorRepeatTypeRule
+typerule BITVECTOR_REPEAT ::cvc5::theory::bv::BitVectorRepeatTypeRule
 typerule BITVECTOR_ROTATE_LEFT_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_ROTATE_LEFT ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_ROTATE_LEFT ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_ROTATE_RIGHT_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_ROTATE_RIGHT ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_ROTATE_RIGHT ::cvc5::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_SIGN_EXTEND_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_SIGN_EXTEND ::CVC5::theory::bv::BitVectorExtendTypeRule
+typerule BITVECTOR_SIGN_EXTEND ::cvc5::theory::bv::BitVectorExtendTypeRule
 typerule BITVECTOR_ZERO_EXTEND_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_ZERO_EXTEND ::CVC5::theory::bv::BitVectorExtendTypeRule
-typerule INT_TO_BITVECTOR_OP ::CVC5::theory::bv::IntToBitVectorOpTypeRule
-typerule INT_TO_BITVECTOR ::CVC5::theory::bv::BitVectorConversionTypeRule
+typerule BITVECTOR_ZERO_EXTEND ::cvc5::theory::bv::BitVectorExtendTypeRule
+typerule INT_TO_BITVECTOR_OP ::cvc5::theory::bv::IntToBitVectorOpTypeRule
+typerule INT_TO_BITVECTOR ::cvc5::theory::bv::BitVectorConversionTypeRule
 
 endtheory
diff --git a/src/theory/bv/proof_checker.cpp b/src/theory/bv/proof_checker.cpp
index 82f37c552..e7ecc0f48 100644
--- a/src/theory/bv/proof_checker.cpp
+++ b/src/theory/bv/proof_checker.cpp
@@ -14,7 +14,7 @@
 
 #include "theory/bv/proof_checker.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -50,4 +50,4 @@ Node BVProofRuleChecker::checkInternal(PfRule id,
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/proof_checker.h b/src/theory/bv/proof_checker.h
index efa319322..b328600df 100644
--- a/src/theory/bv/proof_checker.h
+++ b/src/theory/bv/proof_checker.h
@@ -22,7 +22,7 @@
 #include "expr/proof_node.h"
 #include "theory/bv/bitblast/simple_bitblaster.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -45,6 +45,6 @@ class BVProofRuleChecker : public ProofRuleChecker
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BV__PROOF_CHECKER_H */
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index e8c032a61..75357b76c 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -22,7 +22,7 @@
 
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -83,4 +83,4 @@ std::string Base::debugPrint() const {
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index 56ed0ecba..55a64d92b 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -23,7 +23,7 @@
 #include <vector>
 #include "util/index.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -51,6 +51,6 @@ public:
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BV__SLICER_BV_H */
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 185f7ad2a..8f9f88ea2 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -23,7 +23,7 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/ee_setup_info.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -236,4 +236,4 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions,
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 1608dc3cf..c9ddaad11 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -24,7 +24,7 @@
 #include "theory/theory_eq_notify.h"
 #include "theory/theory_state.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -124,6 +124,6 @@ class TheoryBV : public Theory
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BV__THEORY_BV_H */
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index f9bd4215d..e92ed5543 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -30,7 +30,7 @@
 #include "theory/theory.h"
 #include "util/statistics_registry.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -770,4 +770,4 @@ struct FixpointRewriteStrategy {
 
 } // End namespace bv
 } // End namespace theory
-}  // End namespace CVC5
+}  // End namespace cvc5
diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index 917d77637..5b25eb45d 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -22,7 +22,7 @@
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_utils.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -492,4 +492,4 @@ Node RewriteRule<EvalComp>::apply(TNode node) {
 
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index c24c3ac48..7060b68a9 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -22,7 +22,7 @@
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_utils.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -302,4 +302,4 @@ Node RewriteRule<ReflexivityEq>::apply(TNode node) {
 
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index cf7bc4a8f..4872f8070 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -27,7 +27,7 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -1571,4 +1571,4 @@ inline Node RewriteRule<NormalizeEqPlusNeg>::apply(TNode node)
 
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 3750ef5b0..3244ebb6e 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -23,7 +23,7 @@
 #include "theory/bv/theory_bv_rewrite_rules.h"
 #include "theory/bv/theory_bv_utils.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -788,4 +788,4 @@ inline Node RewriteRule<RedandEliminate>::apply(TNode node)
 
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index c6dcb9f1e..2e99cc467 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -24,7 +24,7 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -2257,4 +2257,4 @@ Node RewriteRule<MultSltMult>::apply(TNode node)
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 9b2d929ed..142afbb3f 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -25,9 +25,9 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/theory.h"
 
-using namespace CVC5;
-using namespace CVC5::theory;
-using namespace CVC5::theory::bv;
+using namespace cvc5;
+using namespace cvc5::theory;
+using namespace cvc5::theory::bv;
 
 TheoryBVRewriter::TheoryBVRewriter() { initializeRewrites(); }
 
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index e6c42f117..0be333ef0 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -22,7 +22,7 @@
 
 #include "theory/theory_rewriter.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -105,6 +105,6 @@ class TheoryBVRewriter : public TheoryRewriter
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BV__THEORY_BV_REWRITER_H */
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 54ed4579b..4de7eed6d 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -21,7 +21,7 @@
 #ifndef CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
 #define CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -450,6 +450,6 @@ class BitVectorAckermanizationUremTypeRule
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 4a68e3724..c2a7f05b6 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -21,7 +21,7 @@
 #include "options/theory_options.h"
 #include "theory/theory.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 namespace utils {
@@ -511,4 +511,4 @@ Node eliminateInt2Bv(TNode node)
 }  // namespace utils
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 5795b5f14..04258d441 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -25,7 +25,7 @@
 
 #include "expr/node_manager.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -226,4 +226,4 @@ Node eliminateInt2Bv(TNode node);
 }
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
index 31fe11715..826b61d6b 100644
--- a/src/theory/bv/type_enumerator.h
+++ b/src/theory/bv/type_enumerator.h
@@ -26,7 +26,7 @@
 #include "util/bitvector.h"
 #include "util/integer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -61,6 +61,6 @@ public:
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BV__TYPE_ENUMERATOR_H */