Rename namespace CVC4 to CVC5. (#6249)

78 files changed, 203 insertions, 205 deletions

diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index 42c386220..ab3e950b9 100644
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -23,7 +23,7 @@
 #include "theory/builtin/proof_checker.h"
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 
 AssertionPipeline::AssertionPipeline()
@@ -212,4 +212,4 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
 }
 
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
index 71a992e3c..454606315 100644
--- a/src/preprocessing/assertion_pipeline.h
+++ b/src/preprocessing/assertion_pipeline.h
@@ -23,7 +23,7 @@
 #include "expr/node.h"
 #include "theory/trust_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofGenerator;
 namespace smt {
@@ -198,6 +198,6 @@ class AssertionPipeline
 }; /* class AssertionPipeline */
 
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__ASSERTION_PIPELINE_H */
diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp
index 198ce6f1f..a67861664 100644
--- a/src/preprocessing/passes/ackermann.cpp
+++ b/src/preprocessing/passes/ackermann.cpp
@@ -32,10 +32,10 @@
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
 
-using namespace CVC4;
-using namespace CVC4::theory;
+using namespace CVC5;
+using namespace CVC5::theory;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -336,4 +336,4 @@ PreprocessingPassResult Ackermann::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/ackermann.h b/src/preprocessing/passes/ackermann.h
index f74d8cb27..e177b4270 100644
--- a/src/preprocessing/passes/ackermann.h
+++ b/src/preprocessing/passes/ackermann.h
@@ -33,7 +33,7 @@
 #include "theory/logic_info.h"
 #include "theory/substitutions.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -82,6 +82,6 @@ class Ackermann : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__ACKERMANN_H */
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index f706ea7e3..16f06540e 100644
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -23,7 +23,7 @@
 #include "theory/rewriter.h"
 #include "theory/substitutions.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -63,4 +63,4 @@ PreprocessingPassResult ApplySubsts::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/apply_substs.h b/src/preprocessing/passes/apply_substs.h
index 7f206387f..6345f35dd 100644
--- a/src/preprocessing/passes/apply_substs.h
+++ b/src/preprocessing/passes/apply_substs.h
@@ -22,7 +22,7 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 
 class PreprocessingPassContext;
@@ -46,6 +46,6 @@ class ApplySubsts : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/preprocessing/passes/bool_to_bv.cpp b/src/preprocessing/passes/bool_to_bv.cpp
index 62c747bc3..042bc3e01 100644
--- a/src/preprocessing/passes/bool_to_bv.cpp
+++ b/src/preprocessing/passes/bool_to_bv.cpp
@@ -26,10 +26,10 @@
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
-using namespace CVC4::theory;
+using namespace CVC5::theory;
 
 BoolToBV::BoolToBV(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "bool-to-bv"), d_statistics()
@@ -422,4 +422,4 @@ BoolToBV::Statistics::~Statistics()
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/bool_to_bv.h b/src/preprocessing/passes/bool_to_bv.h
index 357acd374..885c57302 100644
--- a/src/preprocessing/passes/bool_to_bv.h
+++ b/src/preprocessing/passes/bool_to_bv.h
@@ -23,7 +23,7 @@
 #include "preprocessing/preprocessing_pass.h"
 #include "util/statistics_registry.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -121,6 +121,6 @@ class BoolToBV : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H */
diff --git a/src/preprocessing/passes/bv_abstraction.cpp b/src/preprocessing/passes/bv_abstraction.cpp
index 539cc3b36..045b4295b 100644
--- a/src/preprocessing/passes/bv_abstraction.cpp
+++ b/src/preprocessing/passes/bv_abstraction.cpp
@@ -32,11 +32,11 @@
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
-using namespace CVC4::theory;
+using namespace CVC5::theory;
 
 BvAbstraction::BvAbstraction(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "bv-abstraction"){};
@@ -60,4 +60,4 @@ PreprocessingPassResult BvAbstraction::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/bv_abstraction.h b/src/preprocessing/passes/bv_abstraction.h
index 3e04aa6e1..b16a2f973 100644
--- a/src/preprocessing/passes/bv_abstraction.h
+++ b/src/preprocessing/passes/bv_abstraction.h
@@ -28,7 +28,7 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -44,6 +44,6 @@ class BvAbstraction : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__BV_ABSTRACTION_H */
diff --git a/src/preprocessing/passes/bv_eager_atoms.cpp b/src/preprocessing/passes/bv_eager_atoms.cpp
index 2158a7299..15b7662c4 100644
--- a/src/preprocessing/passes/bv_eager_atoms.cpp
+++ b/src/preprocessing/passes/bv_eager_atoms.cpp
@@ -22,7 +22,7 @@
 #include "theory/theory_engine.h"
 #include "theory/theory_model.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -47,4 +47,4 @@ PreprocessingPassResult BvEagerAtoms::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/bv_eager_atoms.h b/src/preprocessing/passes/bv_eager_atoms.h
index 6fe17115e..a3c7a424a 100644
--- a/src/preprocessing/passes/bv_eager_atoms.h
+++ b/src/preprocessing/passes/bv_eager_atoms.h
@@ -22,7 +22,7 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -38,6 +38,6 @@ class BvEagerAtoms : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__BV_EAGER_ATOMS_H */
diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp
index e1e4b20a2..2ec12256a 100644
--- a/src/preprocessing/passes/bv_gauss.cpp
+++ b/src/preprocessing/passes/bv_gauss.cpp
@@ -28,11 +28,11 @@
 #include "theory/rewriter.h"
 #include "util/bitvector.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;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -704,7 +704,7 @@ PreprocessingPassResult BVGauss::applyInternal(
   {
     Node a = assertions.back();
     assertions.pop_back();
-    CVC4::Kind k = a.getKind();
+    CVC5::Kind k = a.getKind();
 
     if (k == kind::AND)
     {
@@ -800,4 +800,4 @@ PreprocessingPassResult BVGauss::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/bv_gauss.h b/src/preprocessing/passes/bv_gauss.h
index c677a0f87..d06071867 100644
--- a/src/preprocessing/passes/bv_gauss.h
+++ b/src/preprocessing/passes/bv_gauss.h
@@ -23,7 +23,7 @@
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -104,6 +104,6 @@ class BVGauss : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/preprocessing/passes/bv_intro_pow2.cpp b/src/preprocessing/passes/bv_intro_pow2.cpp
index 08fe0cbc9..c611c8af3 100644
--- a/src/preprocessing/passes/bv_intro_pow2.cpp
+++ b/src/preprocessing/passes/bv_intro_pow2.cpp
@@ -25,12 +25,12 @@
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
 using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
-using namespace CVC4::theory;
+using namespace CVC5::theory;
 
 namespace {
 
@@ -100,8 +100,7 @@ PreprocessingPassResult BvIntroPow2::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
+}  // namespace passes
+}  // namespace preprocessing
 
-}/* CVC4::theory::bv namespace */
-}/* CVC4::theory namespace */
-
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/bv_intro_pow2.h b/src/preprocessing/passes/bv_intro_pow2.h
index 870eacf04..98e1efc1d 100644
--- a/src/preprocessing/passes/bv_intro_pow2.h
+++ b/src/preprocessing/passes/bv_intro_pow2.h
@@ -23,7 +23,7 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -39,6 +39,6 @@ class BvIntroPow2 : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__BV_INTRO_POW2_H */
diff --git a/src/preprocessing/passes/bv_to_bool.cpp b/src/preprocessing/passes/bv_to_bool.cpp
index 014ddc170..5153f3b7f 100644
--- a/src/preprocessing/passes/bv_to_bool.cpp
+++ b/src/preprocessing/passes/bv_to_bool.cpp
@@ -30,12 +30,12 @@
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
 using namespace std;
-using namespace CVC4::theory;
+using namespace CVC5::theory;
 
 BVToBool::BVToBool(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "bv-to-bool"),
@@ -310,4 +310,4 @@ BVToBool::Statistics::~Statistics()
 
 }  // passes
 }  // Preprocessing
-}  // CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/bv_to_bool.h b/src/preprocessing/passes/bv_to_bool.h
index 17d02c82a..45fa4a5df 100644
--- a/src/preprocessing/passes/bv_to_bool.h
+++ b/src/preprocessing/passes/bv_to_bool.h
@@ -23,7 +23,7 @@
 #include "preprocessing/preprocessing_pass.h"
 #include "util/statistics_registry.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -73,6 +73,6 @@ class BVToBool : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__BV_TO_BOOL_H */
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index f5e81bb9c..f7a87d51f 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -33,13 +33,13 @@
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
 using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
+using namespace CVC5::theory;
+using namespace CVC5::theory::bv;
 
 namespace {
 
@@ -1046,4 +1046,4 @@ Node BVToInt::createBVNotNode(Node n, uint64_t bvsize)
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h
index 21587a6b4..bc949bff2 100644
--- a/src/preprocessing/passes/bv_to_int.h
+++ b/src/preprocessing/passes/bv_to_int.h
@@ -73,7 +73,7 @@
 #include "preprocessing/preprocessing_pass.h"
 #include "theory/arith/nl/iand_utils.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -285,6 +285,6 @@ class BVToInt : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H */
diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp
index 78898a3dc..245c889d3 100644
--- a/src/preprocessing/passes/extended_rewriter_pass.cpp
+++ b/src/preprocessing/passes/extended_rewriter_pass.cpp
@@ -21,7 +21,7 @@
 #include "preprocessing/preprocessing_pass_context.h"
 #include "theory/quantifiers/extended_rewrite.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -43,4 +43,4 @@ PreprocessingPassResult ExtRewPre::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/extended_rewriter_pass.h b/src/preprocessing/passes/extended_rewriter_pass.h
index 0b921ad46..60ab6af98 100644
--- a/src/preprocessing/passes/extended_rewriter_pass.h
+++ b/src/preprocessing/passes/extended_rewriter_pass.h
@@ -21,7 +21,7 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -37,6 +37,6 @@ class ExtRewPre : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H */
diff --git a/src/preprocessing/passes/foreign_theory_rewrite.cpp b/src/preprocessing/passes/foreign_theory_rewrite.cpp
index b4e6107cc..c1a995469 100644
--- a/src/preprocessing/passes/foreign_theory_rewrite.cpp
+++ b/src/preprocessing/passes/foreign_theory_rewrite.cpp
@@ -22,11 +22,11 @@
 #include "theory/rewriter.h"
 #include "theory/strings/arith_entail.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
-using namespace CVC4::theory;
+using namespace CVC5::theory;
 ForeignTheoryRewrite::ForeignTheoryRewrite(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "foreign-theory-rewrite"),
       d_cache(preprocContext->getUserContext()){};
@@ -149,4 +149,4 @@ PreprocessingPassResult ForeignTheoryRewrite::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/foreign_theory_rewrite.h b/src/preprocessing/passes/foreign_theory_rewrite.h
index c693a1192..e50909617 100644
--- a/src/preprocessing/passes/foreign_theory_rewrite.h
+++ b/src/preprocessing/passes/foreign_theory_rewrite.h
@@ -23,7 +23,7 @@
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -62,6 +62,6 @@ class ForeignTheoryRewrite : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__FOREIGN_THEORY_REWRITE_H */
diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp
index 312437c38..b34df8ca3 100644
--- a/src/preprocessing/passes/fun_def_fmf.cpp
+++ b/src/preprocessing/passes/fun_def_fmf.cpp
@@ -26,11 +26,11 @@
 #include "theory/rewriter.h"
 
 using namespace std;
-using namespace CVC4::kind;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
+using namespace CVC5::kind;
+using namespace CVC5::theory;
+using namespace CVC5::theory::quantifiers;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -466,4 +466,4 @@ void FunDefFmf::getConstraints(Node n,
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/fun_def_fmf.h b/src/preprocessing/passes/fun_def_fmf.h
index 90f3829f6..194c520ab 100644
--- a/src/preprocessing/passes/fun_def_fmf.h
+++ b/src/preprocessing/passes/fun_def_fmf.h
@@ -22,7 +22,7 @@
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -100,6 +100,6 @@ class FunDefFmf : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */
diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp
index 364e44e09..60f584225 100644
--- a/src/preprocessing/passes/global_negate.cpp
+++ b/src/preprocessing/passes/global_negate.cpp
@@ -21,10 +21,10 @@
 #include "theory/rewriter.h"
 
 using namespace std;
-using namespace CVC4::kind;
-using namespace CVC4::theory;
+using namespace CVC5::kind;
+using namespace CVC5::theory;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -124,4 +124,4 @@ PreprocessingPassResult GlobalNegate::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h
index 857664838..2e9dbdcb7 100644
--- a/src/preprocessing/passes/global_negate.h
+++ b/src/preprocessing/passes/global_negate.h
@@ -29,7 +29,7 @@
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -48,6 +48,6 @@ class GlobalNegate : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */
diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp
index 284fbc72b..13a59a92d 100644
--- a/src/preprocessing/passes/ho_elim.cpp
+++ b/src/preprocessing/passes/ho_elim.cpp
@@ -24,9 +24,9 @@
 #include "theory/rewriter.h"
 #include "theory/uf/theory_uf_rewriter.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -539,4 +539,4 @@ TypeNode HoElim::getUSort(TypeNode tn)
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h
index d7a0de599..36aa53acf 100644
--- a/src/preprocessing/passes/ho_elim.h
+++ b/src/preprocessing/passes/ho_elim.h
@@ -26,7 +26,7 @@
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -150,6 +150,6 @@ class HoElim : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* __CVC4__PREPROCESSING__PASSES__HO_ELIM_PASS_H */
diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index e857b7b61..bf59a7311 100644
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -29,12 +29,12 @@
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
 using namespace std;
-using namespace CVC4::theory;
+using namespace CVC5::theory;
 
 using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
 
@@ -267,4 +267,4 @@ PreprocessingPassResult IntToBV::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/int_to_bv.h b/src/preprocessing/passes/int_to_bv.h
index 774d8cb46..a6eda934f 100644
--- a/src/preprocessing/passes/int_to_bv.h
+++ b/src/preprocessing/passes/int_to_bv.h
@@ -23,7 +23,7 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -39,6 +39,6 @@ class IntToBV : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__INT_TO_BV_H */
diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
index afa1d3ba2..91b805004 100644
--- a/src/preprocessing/passes/ite_removal.cpp
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -25,11 +25,11 @@
 #include "theory/rewriter.h"
 #include "theory/theory_preprocessor.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
-using namespace CVC4::theory;
+using namespace CVC5::theory;
 
 // TODO (project #42): note this preprocessing pass is deprecated
 IteRemoval::IteRemoval(PreprocessingPassContext* preprocContext)
@@ -79,4 +79,4 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/ite_removal.h b/src/preprocessing/passes/ite_removal.h
index 3881eab2d..ceb9af4ac 100644
--- a/src/preprocessing/passes/ite_removal.h
+++ b/src/preprocessing/passes/ite_removal.h
@@ -22,7 +22,7 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -37,6 +37,6 @@ class IteRemoval : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif  // CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index e298b39e2..8b9ad9587 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -26,10 +26,10 @@
 #include "theory/theory_engine.h"
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::theory;
+using namespace CVC5;
+using namespace CVC5::theory;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -97,7 +97,7 @@ void compressBeforeRealAssertions(AssertionPipeline* assertionsToPreprocess,
   assertionsToPreprocess->resize(before);
   size_t lastBeforeItes = assertionsToPreprocess->getRealAssertionsEnd() - 1;
   intoConjunction.push_back((*assertionsToPreprocess)[lastBeforeItes]);
-  Node newLast = CVC4::util::NaryBuilder::mkAssoc(kind::AND, intoConjunction);
+  Node newLast = CVC5::util::NaryBuilder::mkAssoc(kind::AND, intoConjunction);
   assertionsToPreprocess->replace(lastBeforeItes, newLast);
   Assert(assertionsToPreprocess->size() == before);
 }
@@ -262,4 +262,4 @@ PreprocessingPassResult ITESimp::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/ite_simp.h b/src/preprocessing/passes/ite_simp.h
index 110ce6057..e5ab27620 100644
--- a/src/preprocessing/passes/ite_simp.h
+++ b/src/preprocessing/passes/ite_simp.h
@@ -21,7 +21,7 @@
 #include "preprocessing/util/ite_utilities.h"
 #include "util/stats_histogram.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -52,6 +52,6 @@ class ITESimp : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index f6ae77bc2..a810d3e19 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -30,12 +30,12 @@
 #include "theory/theory_model.h"
 #include "theory/trust_substitutions.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
 using namespace std;
-using namespace CVC4::theory;
+using namespace CVC5::theory;
 
 namespace {
 
@@ -667,4 +667,4 @@ MipLibTrick::Statistics::~Statistics()
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/miplib_trick.h b/src/preprocessing/passes/miplib_trick.h
index 66622d06a..61bf40040 100644
--- a/src/preprocessing/passes/miplib_trick.h
+++ b/src/preprocessing/passes/miplib_trick.h
@@ -21,7 +21,7 @@
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -57,6 +57,6 @@ class MipLibTrick : public PreprocessingPass, public NodeManagerListener
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__MIPLIB_TRICK_H */
diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp
index 1f85f0caf..3bc8ff8dd 100644
--- a/src/preprocessing/passes/nl_ext_purify.cpp
+++ b/src/preprocessing/passes/nl_ext_purify.cpp
@@ -19,12 +19,12 @@
 #include "preprocessing/assertion_pipeline.h"
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
 using namespace std;
-using namespace CVC4::theory;
+using namespace CVC5::theory;
 
 Node NlExtPurify::purifyNlTerms(TNode n,
                                 NodeMap& cache,
@@ -140,4 +140,4 @@ PreprocessingPassResult NlExtPurify::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/nl_ext_purify.h b/src/preprocessing/passes/nl_ext_purify.h
index c49336308..c9b5c344c 100644
--- a/src/preprocessing/passes/nl_ext_purify.h
+++ b/src/preprocessing/passes/nl_ext_purify.h
@@ -26,7 +26,7 @@
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -51,6 +51,6 @@ class NlExtPurify : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H */
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index b03d21dd9..29e7233c0 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -30,10 +30,10 @@
 #include "theory/theory_model.h"
 #include "theory/trust_substitutions.h"
 
-using namespace CVC4;
-using namespace CVC4::theory;
+using namespace CVC5;
+using namespace CVC5::theory;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -491,4 +491,4 @@ Node NonClausalSimp::processRewrittenLearnedLit(theory::TrustNode trn)
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h
index 27fac3f60..dfaa24a93 100644
--- a/src/preprocessing/passes/non_clausal_simp.h
+++ b/src/preprocessing/passes/non_clausal_simp.h
@@ -22,7 +22,7 @@
 #include "preprocessing/preprocessing_pass.h"
 #include "theory/trust_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class LazyCDProof;
 class ProofNodeManager;
@@ -97,6 +97,6 @@ class NonClausalSimp : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/preprocessing/passes/pseudo_boolean_processor.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp
index bc410a70a..5ce7338f3 100644
--- a/src/preprocessing/passes/pseudo_boolean_processor.cpp
+++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp
@@ -24,12 +24,12 @@
 #include "theory/arith/normal_form.h"
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
-using namespace CVC4::theory;
-using namespace CVC4::theory::arith;
+using namespace CVC5::theory;
+using namespace CVC5::theory::arith;
 
 PseudoBooleanProcessor::PseudoBooleanProcessor(
     PreprocessingPassContext* preprocContext)
@@ -418,4 +418,4 @@ void PseudoBooleanProcessor::clear()
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/pseudo_boolean_processor.h b/src/preprocessing/passes/pseudo_boolean_processor.h
index 84f7f7f31..6e1b426bf 100644
--- a/src/preprocessing/passes/pseudo_boolean_processor.h
+++ b/src/preprocessing/passes/pseudo_boolean_processor.h
@@ -31,7 +31,7 @@
 #include "util/maybe.h"
 #include "util/rational.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -110,6 +110,6 @@ class PseudoBooleanProcessor : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif  // CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp
index f0b51e6a5..b296f9c17 100644
--- a/src/preprocessing/passes/quantifier_macros.cpp
+++ b/src/preprocessing/passes/quantifier_macros.cpp
@@ -35,11 +35,11 @@
 #include "theory/theory_engine.h"
 
 using namespace std;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-using namespace CVC4::kind;
+using namespace CVC5::theory;
+using namespace CVC5::theory::quantifiers;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -568,4 +568,4 @@ void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) {
 
 }  // passes
 }  // preprocessing
-}  // CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h
index 3d6a56396..51b3c7951 100644
--- a/src/preprocessing/passes/quantifier_macros.h
+++ b/src/preprocessing/passes/quantifier_macros.h
@@ -22,7 +22,7 @@
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -91,6 +91,6 @@ class QuantifierMacros : public PreprocessingPass
 
 }  // passes
 }  // preprocessing
-}  // CVC4
+}  // namespace CVC5
 
 #endif /*CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */
diff --git a/src/preprocessing/passes/quantifiers_preprocess.cpp b/src/preprocessing/passes/quantifiers_preprocess.cpp
index af1eb5071..15f0fc54b 100644
--- a/src/preprocessing/passes/quantifiers_preprocess.cpp
+++ b/src/preprocessing/passes/quantifiers_preprocess.cpp
@@ -24,12 +24,12 @@
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
 using namespace std;
-using namespace CVC4::theory;
+using namespace CVC5::theory;
 
 QuantifiersPreprocess::QuantifiersPreprocess(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "quantifiers-preprocess"){};
@@ -58,4 +58,4 @@ PreprocessingPassResult QuantifiersPreprocess::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/quantifiers_preprocess.h b/src/preprocessing/passes/quantifiers_preprocess.h
index 1c0125217..b9ea842cb 100644
--- a/src/preprocessing/passes/quantifiers_preprocess.h
+++ b/src/preprocessing/passes/quantifiers_preprocess.h
@@ -24,7 +24,7 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -40,6 +40,6 @@ class QuantifiersPreprocess : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__QUANTIFIERS_PREPROCESS_H */
diff --git a/src/preprocessing/passes/real_to_int.cpp b/src/preprocessing/passes/real_to_int.cpp
index 9c58250e3..bc8ba0b79 100644
--- a/src/preprocessing/passes/real_to_int.cpp
+++ b/src/preprocessing/passes/real_to_int.cpp
@@ -24,12 +24,12 @@
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
 using namespace std;
-using namespace CVC4::theory;
+using namespace CVC5::theory;
 
 Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& var_eq)
 {
@@ -213,4 +213,4 @@ PreprocessingPassResult RealToInt::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/real_to_int.h b/src/preprocessing/passes/real_to_int.h
index 7bfdfd428..5579e3faf 100644
--- a/src/preprocessing/passes/real_to_int.h
+++ b/src/preprocessing/passes/real_to_int.h
@@ -24,7 +24,7 @@
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -45,6 +45,6 @@ class RealToInt : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__REAL_TO_INT_H */
diff --git a/src/preprocessing/passes/rewrite.cpp b/src/preprocessing/passes/rewrite.cpp
index f1a4ec283..35c2e9926 100644
--- a/src/preprocessing/passes/rewrite.cpp
+++ b/src/preprocessing/passes/rewrite.cpp
@@ -19,12 +19,11 @@
 #include "preprocessing/assertion_pipeline.h"
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
-using namespace CVC4::theory;
-
+using namespace CVC5::theory;
 
 Rewrite::Rewrite(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "rewrite"){};
@@ -43,4 +42,4 @@ PreprocessingPassResult Rewrite::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/rewrite.h b/src/preprocessing/passes/rewrite.h
index 22400911f..4848c8a98 100644
--- a/src/preprocessing/passes/rewrite.h
+++ b/src/preprocessing/passes/rewrite.h
@@ -21,7 +21,7 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -37,7 +37,7 @@ class Rewrite : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__REWRITE_H */
 
diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp
index 381282b38..6100e0762 100644
--- a/src/preprocessing/passes/sep_skolem_emp.cpp
+++ b/src/preprocessing/passes/sep_skolem_emp.cpp
@@ -25,12 +25,12 @@
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
 using namespace std;
-using namespace CVC4::theory;
+using namespace CVC5::theory;
 
 namespace {
 
@@ -124,4 +124,4 @@ PreprocessingPassResult SepSkolemEmp::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/sep_skolem_emp.h b/src/preprocessing/passes/sep_skolem_emp.h
index 51e421505..11e7bec24 100644
--- a/src/preprocessing/passes/sep_skolem_emp.h
+++ b/src/preprocessing/passes/sep_skolem_emp.h
@@ -20,7 +20,7 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -36,6 +36,6 @@ class SepSkolemEmp : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__SEP_SKOLEM_EMP_H */
diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp
index 6e399bcca..07c5e7cc5 100644
--- a/src/preprocessing/passes/sort_infer.cpp
+++ b/src/preprocessing/passes/sort_infer.cpp
@@ -26,7 +26,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -91,4 +91,4 @@ PreprocessingPassResult SortInferencePass::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/sort_infer.h b/src/preprocessing/passes/sort_infer.h
index 74ae0bd2b..5874b4363 100644
--- a/src/preprocessing/passes/sort_infer.h
+++ b/src/preprocessing/passes/sort_infer.h
@@ -17,7 +17,7 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -38,6 +38,6 @@ class SortInferencePass : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__SORT_INFERENCE_PASS_H_ */
diff --git a/src/preprocessing/passes/static_learning.cpp b/src/preprocessing/passes/static_learning.cpp
index 7b49de141..1cc2ce06f 100644
--- a/src/preprocessing/passes/static_learning.cpp
+++ b/src/preprocessing/passes/static_learning.cpp
@@ -23,7 +23,7 @@
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -57,4 +57,4 @@ PreprocessingPassResult StaticLearning::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/static_learning.h b/src/preprocessing/passes/static_learning.h
index e9c5d70f5..67bf053f9 100644
--- a/src/preprocessing/passes/static_learning.h
+++ b/src/preprocessing/passes/static_learning.h
@@ -20,7 +20,7 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -36,6 +36,6 @@ class StaticLearning : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__STATIC_LEARNING_H */
diff --git a/src/preprocessing/passes/strings_eager_pp.cpp b/src/preprocessing/passes/strings_eager_pp.cpp
index 08f6a8de3..775a09441 100644
--- a/src/preprocessing/passes/strings_eager_pp.cpp
+++ b/src/preprocessing/passes/strings_eager_pp.cpp
@@ -18,9 +18,9 @@
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_preprocess.h"
 
-using namespace CVC4::theory;
+using namespace CVC5::theory;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -57,4 +57,4 @@ PreprocessingPassResult StringsEagerPp::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/strings_eager_pp.h b/src/preprocessing/passes/strings_eager_pp.h
index 16324368e..3af59766c 100644
--- a/src/preprocessing/passes/strings_eager_pp.h
+++ b/src/preprocessing/passes/strings_eager_pp.h
@@ -19,7 +19,7 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -39,6 +39,6 @@ class StringsEagerPp : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__STRINGS_EAGER_PP_H */
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index ff60173ed..f05afe54f 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -27,10 +27,10 @@
 #include "theory/smt_engine_subsolver.h"
 
 using namespace std;
-using namespace CVC4::kind;
-using namespace CVC4::theory;
+using namespace CVC5::kind;
+using namespace CVC5::theory;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -345,4 +345,4 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions,
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/sygus_inference.h b/src/preprocessing/passes/sygus_inference.h
index f9d8bf9dd..b31e5ca7c 100644
--- a/src/preprocessing/passes/sygus_inference.h
+++ b/src/preprocessing/passes/sygus_inference.h
@@ -20,7 +20,7 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -63,6 +63,6 @@ class SygusInference : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index bf84ee76e..7213dc8a8 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -30,9 +30,9 @@
 #include "theory/quantifiers/term_util.h"
 
 using namespace std;
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -474,4 +474,4 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/synth_rew_rules.h b/src/preprocessing/passes/synth_rew_rules.h
index 82adde0d6..eb52688e7 100644
--- a/src/preprocessing/passes/synth_rew_rules.h
+++ b/src/preprocessing/passes/synth_rew_rules.h
@@ -18,7 +18,7 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -71,6 +71,6 @@ class SynthRewRulesPass : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__SYNTH_REW_RULES_H */
diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index 1a6abd723..7112dd50f 100644
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -24,11 +24,11 @@
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
-using namespace CVC4::theory;
+using namespace CVC5::theory;
 
 TheoryPreprocess::TheoryPreprocess(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "theory-preprocess"){};
@@ -72,4 +72,4 @@ PreprocessingPassResult TheoryPreprocess::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/theory_preprocess.h b/src/preprocessing/passes/theory_preprocess.h
index fe5dcbd7c..bd450840e 100644
--- a/src/preprocessing/passes/theory_preprocess.h
+++ b/src/preprocessing/passes/theory_preprocess.h
@@ -21,7 +21,7 @@
 
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -37,6 +37,6 @@ class TheoryPreprocess : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__THEORY_PREPROCESS_H */
diff --git a/src/preprocessing/passes/theory_rewrite_eq.cpp b/src/preprocessing/passes/theory_rewrite_eq.cpp
index 79338d63b..c70458b91 100644
--- a/src/preprocessing/passes/theory_rewrite_eq.cpp
+++ b/src/preprocessing/passes/theory_rewrite_eq.cpp
@@ -18,9 +18,9 @@
 #include "preprocessing/preprocessing_pass_context.h"
 #include "theory/theory_engine.h"
 
-using namespace CVC4::theory;
+using namespace CVC5::theory;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -116,4 +116,4 @@ theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n)
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/theory_rewrite_eq.h b/src/preprocessing/passes/theory_rewrite_eq.h
index ada99a7cb..626efe8e3 100644
--- a/src/preprocessing/passes/theory_rewrite_eq.h
+++ b/src/preprocessing/passes/theory_rewrite_eq.h
@@ -21,7 +21,7 @@
 #include "preprocessing/preprocessing_pass.h"
 #include "theory/trust_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
@@ -51,6 +51,6 @@ class TheoryRewriteEq : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H */
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index cf2e96c79..502889dd3 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -26,12 +26,12 @@
 #include "theory/logic_info.h"
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace passes {
 
 using namespace std;
-using namespace CVC4::theory;
+using namespace CVC5::theory;
 
 UnconstrainedSimplifier::UnconstrainedSimplifier(
     PreprocessingPassContext* preprocContext)
@@ -880,4 +880,4 @@ PreprocessingPassResult UnconstrainedSimplifier::applyInternal(
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h
index 5609273da..da368de51 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.h
+++ b/src/preprocessing/passes/unconstrained_simplifier.h
@@ -29,7 +29,7 @@
 #include "theory/substitutions.h"
 #include "util/statistics_registry.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace context {
 class Context;
 }
@@ -72,6 +72,6 @@ class UnconstrainedSimplifier : public PreprocessingPass
 
 }  // namespace passes
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index 5741b19be..127b22758 100644
--- a/src/preprocessing/preprocessing_pass.cpp
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -24,7 +24,7 @@
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 
 PreprocessingPassResult PreprocessingPass::apply(
@@ -70,4 +70,4 @@ PreprocessingPass::~PreprocessingPass() {
 }
 
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
index 498c507d0..f112d5f54 100644
--- a/src/preprocessing/preprocessing_pass.h
+++ b/src/preprocessing/preprocessing_pass.h
@@ -36,7 +36,7 @@
 #include "util/statistics_registry.h"
 #include "util/stats_timer.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 
 class AssertionPipeline;
@@ -81,6 +81,6 @@ class PreprocessingPass {
 };
 
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_H */
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 8cf885c27..3c64ce301 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -18,7 +18,7 @@
 
 #include "expr/node_algorithm.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 
 PreprocessingPassContext::PreprocessingPassContext(
@@ -61,4 +61,4 @@ ProofNodeManager* PreprocessingPassContext::getProofNodeManager()
 }
 
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index d210f6b60..93563e3a2 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -26,7 +26,7 @@
 #include "theory/trust_substitutions.h"
 #include "util/resource_manager.h"
 
-namespace CVC4 {
+namespace CVC5 {
 class SmtEngine;
 class TheoryEngine;
 namespace theory::booleans {
@@ -106,6 +106,6 @@ class PreprocessingPassContext
 };  // class PreprocessingPassContext
 
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H */
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp
index 271a3aba5..a46ce0205 100644
--- a/src/preprocessing/preprocessing_pass_registry.cpp
+++ b/src/preprocessing/preprocessing_pass_registry.cpp
@@ -59,10 +59,10 @@
 #include "preprocessing/passes/unconstrained_simplifier.h"
 #include "preprocessing/preprocessing_pass.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 
-using namespace CVC4::preprocessing::passes;
+using namespace CVC5::preprocessing::passes;
 
 PreprocessingPassRegistry& PreprocessingPassRegistry::getInstance()
 {
@@ -158,4 +158,4 @@ PreprocessingPassRegistry::PreprocessingPassRegistry()
 }
 
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h
index 4dbab05fe..4843b810b 100644
--- a/src/preprocessing/preprocessing_pass_registry.h
+++ b/src/preprocessing/preprocessing_pass_registry.h
@@ -23,7 +23,7 @@
 #include <string>
 #include <unordered_map>
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 
 class PreprocessingPass;
@@ -94,6 +94,6 @@ class PreprocessingPassRegistry {
 };  // class PreprocessingPassRegistry
 
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PREPROCESSING__PREPROCESSING_PASS_REGISTRY_H */
diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp
index 59c6184de..2b215f9b4 100644
--- a/src/preprocessing/util/ite_utilities.cpp
+++ b/src/preprocessing/util/ite_utilities.cpp
@@ -28,7 +28,7 @@
 #include "theory/theory.h"
 
 using namespace std;
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 namespace util {
 
@@ -1909,4 +1909,4 @@ ITECareSimplifier::CareSetPtr ITECareSimplifier::CareSetPtr::mkNew(
 
 }  // namespace util
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/preprocessing/util/ite_utilities.h b/src/preprocessing/util/ite_utilities.h
index 90c240478..ff58bbacf 100644
--- a/src/preprocessing/util/ite_utilities.h
+++ b/src/preprocessing/util/ite_utilities.h
@@ -31,7 +31,7 @@
 #include "util/statistics_registry.h"
 #include "util/stats_histogram.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace preprocessing {
 
 class AssertionPipeline;
@@ -417,6 +417,6 @@ class ITECareSimplifier
 
 }  // namespace util
 }  // namespace preprocessing
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif