Rename namespace CVC4 to CVC5. (#6249)

57 files changed, 232 insertions, 233 deletions

diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index 3b9df3518..ee4b467b8 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 CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
-using namespace CVC4::context;
+using namespace CVC5;
+using namespace CVC5::theory;
+using namespace CVC5::theory::bv;
+using namespace CVC5::context;
 
 using namespace std;
-using namespace CVC4::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 e22e221f2..6c36de34c 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -246,6 +246,6 @@ public:
 
 }
 }
-}
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index 465a8eb65..002a4f631 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 CVC4 {
+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[] = "CVC4::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 CVC4
+}  // 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 d3326f853..3eccbd3ec 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 CVC4 {
+namespace CVC5 {
 namespace prop {
 class SatSolver;
 }
@@ -121,6 +121,6 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*>
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // 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 01eabfab5..7ae55015f 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 CVC4 {
+namespace CVC5 {
 
 namespace theory {
 namespace bv {
@@ -899,6 +899,6 @@ void DefaultRotateLeftBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb)
 
 }
 }
-}
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/bv/bitblast/bitblast_utils.h b/src/theory/bv/bitblast/bitblast_utils.h
index 37618bd06..e342d4410 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 CVC4 {
+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 CVC4
+}  // 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 738f511b6..90ea5ac2b 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -268,6 +268,6 @@ Node TBitblaster<T>::getTermModel(TNode node, bool fullModel)
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // 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 bbddf82cd..5e22262e2 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -288,4 +288,4 @@ bool EagerBitblaster::isSharedTerm(TNode node) {
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index d66b46505..dead462b5 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -85,5 +85,5 @@ class BitblastingRegistrar : public prop::Registrar
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // 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 7e36f63dd..e20a6f6b5 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -590,4 +590,4 @@ void TLazyBitblaster::clearSolver() {
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index 622369043..1a963e67d 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 CVC4 {
+namespace CVC5 {
 namespace prop {
 class CnfStream;
 class NullRegistrat;
@@ -176,5 +176,5 @@ class TLazyBitblaster : public TBitblaster<Node>
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // 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 4210c4a86..b0cf68609 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -84,4 +84,4 @@ bool BBProof::collectModelValues(TheoryModel* m,
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h
index 6c4c04349..894a9a916 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -47,5 +47,5 @@ class BBProof
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 #endif
diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp
index 10eac275e..76677e2db 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -155,4 +155,4 @@ bool BBSimple::isVariable(TNode node)
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h
index d337dbc08..1b48f9a68 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -75,6 +75,6 @@ class BBSimple : public TBitblaster<Node>
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index e71b200c6..9c478791c 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -125,4 +125,4 @@ bool EagerBitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel)
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 6a1d61a3b..0fe1ed32b 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -60,6 +60,6 @@ class EagerBitblastSolver {
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // 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 1caae9b5e..67554525a 100644
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -18,16 +18,15 @@
 #include "theory/bv/theory_bv_utils.h"
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
-using namespace CVC4::theory::bv::utils;
-
-const TermId CVC4::theory::bv::UndefinedTermId = -1; 
-const ReasonId CVC4::theory::bv::UndefinedReasonId = -1;
-const ReasonId CVC4::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 be5da70b2..caa7220cf 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -291,6 +291,6 @@ public:
 
 }
 }
-}
+}  // 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 36e77b0b7..bbb2f1ca9 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 CVC4::prop;
+using namespace CVC5::prop;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -381,4 +381,4 @@ QuickXPlain::Statistics::~Statistics() {
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index f509c3cb4..3d30d912d 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 
 class TheoryModel;
@@ -181,6 +181,6 @@ class QuickXPlain
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // 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 d79f69e53..f08f7527a 100644
--- a/src/theory/bv/bv_solver.h
+++ b/src/theory/bv/bv_solver.h
@@ -21,7 +21,7 @@
 
 #include "theory/theory.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -117,6 +117,6 @@ class BVSolver
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // 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 e6dfd8286..16a99c2e4 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -281,4 +281,4 @@ Node BVSolverBitblast::getValue(TNode node)
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h
index d1252659a..794b9fa9b 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 CVC4 {
+namespace CVC5 {
 
 namespace theory {
 namespace bv {
@@ -143,6 +143,6 @@ class BVSolverBitblast : public BVSolver
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index 9562b69c7..ed71fccbe 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 CVC4::theory::bv::utils;
+using namespace CVC5::theory::bv::utils;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -828,4 +828,4 @@ void BVSolverLazy::setConflict(Node conflict)
 
 }  // namespace bv
 }  // namespace theory
-} /* namespace CVC4 */
+} // namespace CVC5
diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h
index 4c769fb7a..6511900eb 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -229,6 +229,6 @@ class BVSolverLazy : public BVSolver
 }  // namespace bv
 }  // namespace theory
 
-}  // namespace CVC4
+}  // 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 db89c29bb..65d46e861 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -151,4 +151,4 @@ bool BVSolverSimple::collectModelValues(TheoryModel* m,
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h
index a34ec98ad..1b6976abb 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 CVC4 {
+namespace CVC5 {
 
 namespace theory {
 namespace bv {
@@ -81,6 +81,6 @@ class BVSolverSimple : public BVSolver
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index d4bba4c5e..e558ea7c7 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 CVC4 {
+namespace CVC5 {
 
 namespace theory {
 
@@ -107,6 +107,6 @@ class SubtheorySolver {
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // 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 8f774e552..2343d72d1 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 CVC4::context;
-using namespace CVC4::prop;
-using namespace CVC4::theory::bv::utils;
+using namespace CVC5::context;
+using namespace CVC5::prop;
+using namespace CVC5::theory::bv::utils;
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -990,6 +990,6 @@ Node mergeExplanations(TNode expl1, TNode expl2) {
   return mergeExplanations(expls);
 }
 
-} /* namespace CVC4::theory::bv */
+}  // namespace bv
 } /* namespace CVc4::theory */
-} /* namespace CVC4 */
+} // namespace CVC5
diff --git a/src/theory/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index 71db94cf8..e7156a33e 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -245,4 +245,4 @@ class AlgebraicSolver : public SubtheorySolver
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 89bca151e..2d21a8f0c 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 CVC4::context;
+using namespace CVC5::context;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -276,6 +276,6 @@ void BitblastSolver::setConflict(TNode conflict)
   d_bv->setConflict(final_conflict);
 }
 
-}/* namespace CVC4::theory::bv */
-}/* namespace CVC4::theory */
-}/* namespace CVC4 */
+}  // namespace bv
+}  // namespace theory
+} // namespace CVC5
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index ca6e53dea..f964fb995 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 CVC4 {
+namespace CVC5 {
 
 namespace theory {
 namespace bv {
@@ -83,4 +83,4 @@ class BitblastSolver : public SubtheorySolver
 
 }  // namespace bv
 }  // namespace theory
-} /* namespace CVC4 */
+} // namespace CVC5
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index bda3393e5..486adfdb7 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 CVC4;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
-using namespace CVC4::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 969ded528..700d8c4f5 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -164,4 +164,4 @@ class CoreSolver : public SubtheorySolver {
 
 }
 }
-}
+}  // namespace CVC5
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index aa3607a66..d67a5c550 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 CVC4;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
-using namespace CVC4::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 277449026..232c8676e 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -89,6 +89,6 @@ class InequalitySolver : public SubtheorySolver
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // 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 80f47509e..65a8b5480 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 CVC4 {
+namespace CVC5 {
 
 /*
 ** Converts bit-vector formulas to integer formulas.
@@ -349,6 +349,6 @@ class IntBlaster
   bool d_introduceFreshIntVars;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* __CVC4__THEORY__BV__INT_BLASTER_H */
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 32e0e9e85..884ee49e6 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -4,36 +4,36 @@
 # src/theory/builtin/kinds.
 #
 
-theory THEORY_BV ::CVC4::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 ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
+rewriter ::CVC5::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
 
 constant BITVECTOR_TYPE \
-	::CVC4::BitVectorSize \
-	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSize >" \
+	::CVC5::BitVectorSize \
+	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorSize >" \
 	"util/bitvector.h" \
 	"bit-vector type"
 cardinality BITVECTOR_TYPE \
-	"::CVC4::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \
+	"::CVC5::theory::bv::CardinalityComputer::computeCardinality(%TYPE%)" \
 	"theory/bv/theory_bv_type_rules.h"
 
 constant CONST_BITVECTOR \
-    ::CVC4::BitVector \
-    ::CVC4::BitVectorHashFunction \
+    ::CVC5::BitVector \
+    ::CVC5::BitVectorHashFunction \
     "util/bitvector.h" \
-    "a fixed-width bit-vector constant; payload is an instance of the CVC4::BitVector class"
+    "a fixed-width bit-vector constant; payload is an instance of the CVC5::BitVector class"
 
 enumerator BITVECTOR_TYPE \
-    "::CVC4::theory::bv::BitVectorEnumerator" \
+    "::CVC5::theory::bv::BitVectorEnumerator" \
     "theory/bv/type_enumerator.h"
 
 well-founded BITVECTOR_TYPE \
     true \
-    "(*CVC4::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 \
-	::CVC4::BitVectorBitOf \
-	::CVC4::BitVectorBitOfHashFunction \
+	::CVC5::BitVectorBitOf \
+	::CVC5::BitVectorBitOfHashFunction \
 	"util/bitvector.h" \
-	"operator for the bit-vector boolean bit extract; payload is an instance of the CVC4::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 \
-	::CVC4::BitVectorExtract \
-	::CVC4::BitVectorExtractHashFunction \
+	::CVC5::BitVectorExtract \
+	::CVC5::BitVectorExtractHashFunction \
 	"util/bitvector.h" \
-	"operator for the bit-vector extract; payload is an instance of the CVC4::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 \
-	::CVC4::BitVectorRepeat \
-	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRepeat >" \
+	::CVC5::BitVectorRepeat \
+	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorRepeat >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector repeat; payload is an instance of the CVC4::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 \
-	::CVC4::BitVectorRotateLeft \
-	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateLeft >" \
+	::CVC5::BitVectorRotateLeft \
+	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorRotateLeft >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector rotate left; payload is an instance of the CVC4::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 \
-	::CVC4::BitVectorRotateRight \
-	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateRight >" \
+	::CVC5::BitVectorRotateRight \
+	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorRotateRight >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector rotate right; payload is an instance of the CVC4::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 \
-	::CVC4::BitVectorSignExtend \
-	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSignExtend >" \
+	::CVC5::BitVectorSignExtend \
+	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorSignExtend >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector sign-extend; payload is an instance of the CVC4::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 \
-	::CVC4::BitVectorZeroExtend \
-	"::CVC4::UnsignedHashFunction< ::CVC4::BitVectorZeroExtend >" \
+	::CVC5::BitVectorZeroExtend \
+	"::CVC5::UnsignedHashFunction< ::CVC5::BitVectorZeroExtend >" \
 	"util/bitvector.h" \
-	"operator for the bit-vector zero-extend; payload is an instance of the CVC4::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 \
-	::CVC4::IntToBitVector \
-	"::CVC4::UnsignedHashFunction< ::CVC4::IntToBitVector >" \
+	::CVC5::IntToBitVector \
+	"::CVC5::UnsignedHashFunction< ::CVC5::IntToBitVector >" \
 	"util/bitvector.h" \
-	"operator for the integer conversion to bit-vector; payload is an instance of the CVC4::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 ::CVC4::theory::bv::BitVectorConstantTypeRule
+typerule CONST_BITVECTOR ::CVC5::theory::bv::BitVectorConstantTypeRule
 
 ## concatentation kind
-typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatTypeRule
+typerule BITVECTOR_CONCAT ::CVC5::theory::bv::BitVectorConcatTypeRule
 
 ## bit-wise kinds
-typerule BITVECTOR_AND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorBVPredTypeRule
-typerule BITVECTOR_NAND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_NOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_NOT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_OR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_XNOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_XOR ::CVC4::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 ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_NEG ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_PLUS ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SUB ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_UDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_UREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SMOD ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SREM ::CVC4::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 ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_LSHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SHL ::CVC4::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 ::CVC4::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_ULT ::CVC4::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_UGE ::CVC4::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_UGT ::CVC4::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_SLT ::CVC4::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule
-typerule BITVECTOR_SGT ::CVC4::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 ::CVC4::theory::bv::BitVectorBVPredTypeRule
-typerule BITVECTOR_SLTBV ::CVC4::theory::bv::BitVectorBVPredTypeRule
+typerule BITVECTOR_ULTBV ::CVC5::theory::bv::BitVectorBVPredTypeRule
+typerule BITVECTOR_SLTBV ::CVC5::theory::bv::BitVectorBVPredTypeRule
 
 ## if-then-else kind
-typerule BITVECTOR_ITE ::CVC4::theory::bv::BitVectorITETypeRule
+typerule BITVECTOR_ITE ::CVC5::theory::bv::BitVectorITETypeRule
 
 ## reduction kinds
-typerule BITVECTOR_REDAND ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule
-typerule BITVECTOR_REDOR ::CVC4::theory::bv::BitVectorUnaryPredicateTypeRule
+typerule BITVECTOR_REDAND ::CVC5::theory::bv::BitVectorUnaryPredicateTypeRule
+typerule BITVECTOR_REDOR ::CVC5::theory::bv::BitVectorUnaryPredicateTypeRule
 
 ## conversion kinds
-typerule BITVECTOR_TO_NAT ::CVC4::theory::bv::BitVectorConversionTypeRule
+typerule BITVECTOR_TO_NAT ::CVC5::theory::bv::BitVectorConversionTypeRule
 
 ## internal kinds
-typerule BITVECTOR_ACKERMANNIZE_UDIV ::CVC4::theory::bv::BitVectorAckermanizationUdivTypeRule
-typerule BITVECTOR_ACKERMANNIZE_UREM ::CVC4::theory::bv::BitVectorAckermanizationUremTypeRule
-typerule BITVECTOR_EAGER_ATOM ::CVC4::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 ::CVC4::theory::bv::BitVectorBitOfTypeRule
+typerule BITVECTOR_BITOF ::CVC5::theory::bv::BitVectorBitOfTypeRule
 typerule BITVECTOR_EXTRACT_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule
+typerule BITVECTOR_EXTRACT ::CVC5::theory::bv::BitVectorExtractTypeRule
 typerule BITVECTOR_REPEAT_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule
+typerule BITVECTOR_REPEAT ::CVC5::theory::bv::BitVectorRepeatTypeRule
 typerule BITVECTOR_ROTATE_LEFT_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_ROTATE_LEFT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_ROTATE_LEFT ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_ROTATE_RIGHT_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_ROTATE_RIGHT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_ROTATE_RIGHT ::CVC5::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_SIGN_EXTEND_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
+typerule BITVECTOR_SIGN_EXTEND ::CVC5::theory::bv::BitVectorExtendTypeRule
 typerule BITVECTOR_ZERO_EXTEND_OP "SimpleTypeRule<RBuiltinOperator>"
-typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
-typerule INT_TO_BITVECTOR_OP ::CVC4::theory::bv::IntToBitVectorOpTypeRule
-typerule INT_TO_BITVECTOR ::CVC4::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 862e2034a..82f37c552 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -50,4 +50,4 @@ Node BVProofRuleChecker::checkInternal(PfRule id,
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/bv/proof_checker.h b/src/theory/bv/proof_checker.h
index 119aa4924..efa319322 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -45,6 +45,6 @@ class BVProofRuleChecker : public ProofRuleChecker
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__BV__PROOF_CHECKER_H */
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index a19c18df8..e8c032a61 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -20,9 +20,9 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 
-using namespace std; 
+using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -83,4 +83,4 @@ std::string Base::debugPrint() const {
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index 49c3cfaa7..56ed0ecba 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -23,7 +23,7 @@
 #include <vector>
 #include "util/index.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -47,10 +47,10 @@ public:
     }
     return true; 
   }
-}; 
+};
 
-}/* CVC4::theory::bv namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace bv
+}  // namespace theory
+}  // 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 3d8a5d3ea..185f7ad2a 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -236,4 +236,4 @@ bool TheoryBV::applyAbstraction(const std::vector<Node>& assertions,
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 93e03e5ca..1608dc3cf 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -124,6 +124,6 @@ class TheoryBV : public Theory
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // 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 6cf1934f0..f9bd4215d 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -770,4 +770,4 @@ struct FixpointRewriteStrategy {
 
 } // End namespace bv
 } // End namespace theory
-} // End namespace CVC4
+}  // 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 57cb5f28e..917d77637 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -492,4 +492,4 @@ Node RewriteRule<EvalComp>::apply(TNode node) {
 
 }
 }
-}
+}  // 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 c1aa034e8..c24c3ac48 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -302,4 +302,4 @@ Node RewriteRule<ReflexivityEq>::apply(TNode node) {
 
 }
 }
-}
+}  // 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 db8e588e4..cf7bc4a8f 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -1571,4 +1571,4 @@ inline Node RewriteRule<NormalizeEqPlusNeg>::apply(TNode node)
 
 }
 }
-}
+}  // 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 1272f303d..3750ef5b0 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -788,4 +788,4 @@ inline Node RewriteRule<RedandEliminate>::apply(TNode node)
 
 }
 }
-}
+}  // 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 bbf7c62e7..c6dcb9f1e 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -2257,4 +2257,4 @@ Node RewriteRule<MultSltMult>::apply(TNode node)
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 614261e34..9b2d929ed 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 CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::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 9ecc25973..e6c42f117 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -103,8 +103,8 @@ class TheoryBVRewriter : public TheoryRewriter
   RewriteFunction d_rewriteTable[kind::LAST_KIND];
 }; /* class TheoryBVRewriter */
 
-}/* CVC4::theory::bv namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace bv
+}  // namespace theory
+}  // 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 54e8c6175..54ed4579b 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -450,6 +450,6 @@ class BitVectorAckermanizationUremTypeRule
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC4
+}  // 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 1a6b7a873..4a68e3724 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 namespace utils {
@@ -508,7 +508,7 @@ Node eliminateInt2Bv(TNode node)
   return Node(result);
 }
 
-}/* CVC4::theory::bv::utils namespace */
-}/* CVC4::theory::bv namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace utils
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC5
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index c6c03e561..5795b5f14 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -226,4 +226,4 @@ Node eliminateInt2Bv(TNode node);
 }
 }
 }
-}
+}  // namespace CVC5
diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
index 58f8f5b80..31fe11715 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 CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace bv {
 
@@ -59,8 +59,8 @@ public:
   bool isFinished() override { return d_bits != d_bits.modByPow2(d_size); }
 };/* BitVectorEnumerator */
 
-}/* CVC4::theory::bv namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__BV__TYPE_ENUMERATOR_H */