Rename namespace CVC4 to CVC5. (#6249)

73 files changed, 182 insertions, 183 deletions

diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index c4ecfbbfa..7fd22fb76 100644
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -29,12 +29,12 @@ namespace std {
 template <typename T>
 std::ostream& operator<<(std::ostream& os, const std::vector<T>& v)
 {
-  CVC4::container_to_stream(os, v);
+  CVC5::container_to_stream(os, v);
   return os;
 }
 }  // namespace std
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -545,6 +545,6 @@ void CDCAC::pruneRedundantIntervals(std::vector<CACInterval>& intervals)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index 15230d14c..2b607ae78 100644
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -31,7 +31,7 @@
 #include "theory/arith/nl/cad/proof_generator.h"
 #include "theory/arith/nl/cad/variable_ordering.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -210,7 +210,7 @@ class CDCAC
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
 
diff --git a/src/theory/arith/nl/cad/cdcac_utils.cpp b/src/theory/arith/nl/cad/cdcac_utils.cpp
index 24bad8d60..f40d528ff 100644
--- a/src/theory/arith/nl/cad/cdcac_utils.cpp
+++ b/src/theory/arith/nl/cad/cdcac_utils.cpp
@@ -20,7 +20,7 @@
 
 #include "theory/arith/nl/cad/projections.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -370,6 +370,6 @@ void makeFinestSquareFreeBasis(CACInterval& lhs, CACInterval& rhs)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/cad/cdcac_utils.h b/src/theory/arith/nl/cad/cdcac_utils.h
index dad9bbd7a..3b3a3638b 100644
--- a/src/theory/arith/nl/cad/cdcac_utils.h
+++ b/src/theory/arith/nl/cad/cdcac_utils.h
@@ -28,7 +28,7 @@
 #include "expr/node.h"
 #include "theory/arith/nl/cad/projections.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -105,7 +105,7 @@ void makeFinestSquareFreeBasis(CACInterval& lhs, CACInterval& rhs);
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
 
diff --git a/src/theory/arith/nl/cad/constraints.cpp b/src/theory/arith/nl/cad/constraints.cpp
index 028a61833..1ea172d11 100644
--- a/src/theory/arith/nl/cad/constraints.cpp
+++ b/src/theory/arith/nl/cad/constraints.cpp
@@ -23,7 +23,7 @@
 #include "theory/arith/nl/poly_conversion.h"
 #include "util/poly_util.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -79,6 +79,6 @@ void Constraints::sortConstraints()
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h
index 42f8920c8..70c52e85c 100644
--- a/src/theory/arith/nl/cad/constraints.h
+++ b/src/theory/arith/nl/cad/constraints.h
@@ -28,7 +28,7 @@
 
 #include "theory/arith/nl/poly_conversion.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -87,7 +87,7 @@ class Constraints
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
 
diff --git a/src/theory/arith/nl/cad/projections.cpp b/src/theory/arith/nl/cad/projections.cpp
index 5d72f5a2e..b9e17f844 100644
--- a/src/theory/arith/nl/cad/projections.cpp
+++ b/src/theory/arith/nl/cad/projections.cpp
@@ -20,7 +20,7 @@
 
 #include "base/check.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -106,6 +106,6 @@ PolyVector projection_mccallum(const std::vector<Polynomial>& polys)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h
index 33267cb7a..3b8eb412f 100644
--- a/src/theory/arith/nl/cad/projections.h
+++ b/src/theory/arith/nl/cad/projections.h
@@ -25,7 +25,7 @@
 
 #include <vector>
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -76,7 +76,7 @@ PolyVector projectionMcCallum(const std::vector<poly::Polynomial>& polys);
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
 
diff --git a/src/theory/arith/nl/cad/proof_checker.cpp b/src/theory/arith/nl/cad/proof_checker.cpp
index 45c43e2aa..f1ab2d6a9 100644
--- a/src/theory/arith/nl/cad/proof_checker.cpp
+++ b/src/theory/arith/nl/cad/proof_checker.cpp
@@ -17,9 +17,9 @@
 #include "expr/sequence.h"
 #include "theory/rewriter.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -58,4 +58,4 @@ Node CADProofRuleChecker::checkInternal(PfRule id,
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h
index 5ebe0c6b7..26bbcc3a9 100644
--- a/src/theory/arith/nl/cad/proof_checker.h
+++ b/src/theory/arith/nl/cad/proof_checker.h
@@ -20,7 +20,7 @@
 #include "expr/node.h"
 #include "expr/proof_checker.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -53,6 +53,6 @@ class CADProofRuleChecker : public ProofRuleChecker
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */
diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp
index 9f0799e7c..fe3734dce 100644
--- a/src/theory/arith/nl/cad/proof_generator.cpp
+++ b/src/theory/arith/nl/cad/proof_generator.cpp
@@ -19,7 +19,7 @@
 #include "theory/lazy_tree_proof_generator.h"
 #include "theory/arith/nl/poly_conversion.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -230,6 +230,6 @@ std::ostream& operator<<(std::ostream& os, const CADProofGenerator& proof)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h
index 4709b8e59..c1bb4be1e 100644
--- a/src/theory/arith/nl/cad/proof_generator.h
+++ b/src/theory/arith/nl/cad/proof_generator.h
@@ -28,7 +28,7 @@
 #include "theory/arith/nl/cad/cdcac_utils.h"
 #include "theory/lazy_tree_proof_generator.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofGenerator;
 
@@ -144,7 +144,7 @@ std::ostream& operator<<(std::ostream& os, const CADProofGenerator& proof);
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
 #endif
diff --git a/src/theory/arith/nl/cad/variable_ordering.cpp b/src/theory/arith/nl/cad/variable_ordering.cpp
index 958191fe1..63db35553 100644
--- a/src/theory/arith/nl/cad/variable_ordering.cpp
+++ b/src/theory/arith/nl/cad/variable_ordering.cpp
@@ -20,7 +20,7 @@
 
 #include "util/poly_util.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -132,6 +132,6 @@ std::vector<poly::Variable> VariableOrdering::operator()(
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/cad/variable_ordering.h b/src/theory/arith/nl/cad/variable_ordering.h
index 43e85b3cb..7fda3faa4 100644
--- a/src/theory/arith/nl/cad/variable_ordering.h
+++ b/src/theory/arith/nl/cad/variable_ordering.h
@@ -26,7 +26,7 @@
 #include "theory/arith/nl/cad/constraints.h"
 #include "util/poly_util.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -65,7 +65,7 @@ std::vector<poly_utils::VariableInformation> collectInformation(
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
 
diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp
index c72c9d48d..dc18fbdf5 100644
--- a/src/theory/arith/nl/cad_solver.cpp
+++ b/src/theory/arith/nl/cad_solver.cpp
@@ -20,7 +20,7 @@
 #include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/poly_conversion.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -212,4 +212,4 @@ bool CadSolver::constructModelIfAvailable(std::vector<Node>& assertions)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h
index b83398cd6..de97c48cc 100644
--- a/src/theory/arith/nl/cad_solver.h
+++ b/src/theory/arith/nl/cad_solver.h
@@ -22,7 +22,7 @@
 #include "theory/arith/nl/cad/cdcac.h"
 #include "theory/arith/nl/cad/proof_checker.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofNodeManager;
 
@@ -110,6 +110,6 @@ class CadSolver
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__ARITH__CAD_SOLVER_H */
diff --git a/src/theory/arith/nl/ext/constraint.cpp b/src/theory/arith/nl/ext/constraint.cpp
index 9ec3b1fc1..41331d041 100644
--- a/src/theory/arith/nl/ext/constraint.cpp
+++ b/src/theory/arith/nl/ext/constraint.cpp
@@ -18,9 +18,9 @@
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/nl/ext/monomial.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -123,4 +123,4 @@ bool ConstraintDb::isMaximal(Node atom, Node x) const
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/ext/constraint.h b/src/theory/arith/nl/ext/constraint.h
index d5ed7ccfd..9e6451c99 100644
--- a/src/theory/arith/nl/ext/constraint.h
+++ b/src/theory/arith/nl/ext/constraint.h
@@ -21,7 +21,7 @@
 #include "expr/kind.h"
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -84,6 +84,6 @@ class ConstraintDb
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__ARITH__NL_SOLVER_H */
diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp
index 28373223b..fc806199e 100644
--- a/src/theory/arith/nl/ext/ext_state.cpp
+++ b/src/theory/arith/nl/ext/ext_state.cpp
@@ -23,8 +23,7 @@
 #include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/nl_lemma_utils.h"
 
-
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -110,4 +109,4 @@ CDProof* ExtState::getProof()
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h
index 46ccaeb14..1d8e7ea0a 100644
--- a/src/theory/arith/nl/ext/ext_state.h
+++ b/src/theory/arith/nl/ext/ext_state.h
@@ -21,7 +21,7 @@
 #include "expr/proof_set.h"
 #include "theory/arith/nl/ext/monomial.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class CDProof;
 
@@ -91,6 +91,6 @@ struct ExtState
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp
index 7a0da42aa..675368843 100644
--- a/src/theory/arith/nl/ext/factoring_check.cpp
+++ b/src/theory/arith/nl/ext/factoring_check.cpp
@@ -23,7 +23,7 @@
 #include "theory/arith/nl/ext/ext_state.h"
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -207,4 +207,4 @@ Node FactoringCheck::getFactorSkolem(Node n, CDProof* proof)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/ext/factoring_check.h b/src/theory/arith/nl/ext/factoring_check.h
index 4c017d198..89c5fce30 100644
--- a/src/theory/arith/nl/ext/factoring_check.h
+++ b/src/theory/arith/nl/ext/factoring_check.h
@@ -19,7 +19,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class CDProof;
 
@@ -69,6 +69,6 @@ class FactoringCheck
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/ext/monomial.cpp b/src/theory/arith/nl/ext/monomial.cpp
index a0d388dca..86abed70c 100644
--- a/src/theory/arith/nl/ext/monomial.cpp
+++ b/src/theory/arith/nl/ext/monomial.cpp
@@ -18,9 +18,9 @@
 #include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/rewriter.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -333,4 +333,4 @@ Node MonomialDb::mkMonomialRemFactor(Node n,
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/ext/monomial.h b/src/theory/arith/nl/ext/monomial.h
index 19f855233..98083b996 100644
--- a/src/theory/arith/nl/ext/monomial.h
+++ b/src/theory/arith/nl/ext/monomial.h
@@ -20,7 +20,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -144,6 +144,6 @@ class MonomialDb
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__ARITH__NL_MONOMIAL_H */
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index f1a2f45b9..c8194bbd0 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -24,7 +24,7 @@
 #include "theory/arith/nl/nl_model.h"
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -520,4 +520,4 @@ void MonomialBoundsCheck::checkResBounds()
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.h b/src/theory/arith/nl/ext/monomial_bounds_check.h
index e7ba4d861..e63dd454a 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.h
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.h
@@ -18,7 +18,7 @@
 #include "expr/node.h"
 #include "theory/arith/nl/ext/constraint.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -86,6 +86,6 @@ class MonomialBoundsCheck
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
index 7f99b876d..9fc2ba10a 100644
--- a/src/theory/arith/nl/ext/monomial_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -22,7 +22,7 @@
 #include "theory/arith/nl/nl_lemma_utils.h"
 #include "theory/arith/nl/ext/ext_state.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -757,4 +757,4 @@ void MonomialCheck::setMonomialFactor(Node a,
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h
index a08554476..948368542 100644
--- a/src/theory/arith/nl/ext/monomial_check.h
+++ b/src/theory/arith/nl/ext/monomial_check.h
@@ -19,7 +19,7 @@
 #include "theory/arith/nl/ext/monomial.h"
 #include "theory/theory_inference.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -194,6 +194,6 @@ class MonomialCheck
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp
index ca600ad55..26db3c9e0 100644
--- a/src/theory/arith/nl/ext/proof_checker.cpp
+++ b/src/theory/arith/nl/ext/proof_checker.cpp
@@ -18,9 +18,9 @@
 #include "theory/arith/arith_utilities.h"
 #include "theory/rewriter.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -158,4 +158,4 @@ Node ExtProofRuleChecker::checkInternal(PfRule id,
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/ext/proof_checker.h b/src/theory/arith/nl/ext/proof_checker.h
index d53b674b2..7bd4b7e38 100644
--- a/src/theory/arith/nl/ext/proof_checker.h
+++ b/src/theory/arith/nl/ext/proof_checker.h
@@ -21,7 +21,7 @@
 #include "expr/proof_checker.h"
 #include "expr/proof_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -51,6 +51,6 @@ class ExtProofRuleChecker : public ProofRuleChecker
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */
diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp
index 45f4160a0..543b6a0bd 100644
--- a/src/theory/arith/nl/ext/split_zero_check.cpp
+++ b/src/theory/arith/nl/ext/split_zero_check.cpp
@@ -22,7 +22,7 @@
 #include "theory/arith/nl/ext/ext_state.h"
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -57,4 +57,4 @@ void SplitZeroCheck::check()
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h
index 030445737..316e304ff 100644
--- a/src/theory/arith/nl/ext/split_zero_check.h
+++ b/src/theory/arith/nl/ext/split_zero_check.h
@@ -18,7 +18,7 @@
 #include "expr/node.h"
 #include "context/cdhashset.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -50,6 +50,6 @@ class SplitZeroCheck
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp
index 64ea19f3c..bdeca7a29 100644
--- a/src/theory/arith/nl/ext/tangent_plane_check.cpp
+++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp
@@ -22,7 +22,7 @@
 #include "theory/arith/nl/ext/ext_state.h"
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -164,4 +164,4 @@ void TangentPlaneCheck::check(bool asWaitingLemmas)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/ext/tangent_plane_check.h b/src/theory/arith/nl/ext/tangent_plane_check.h
index a771ae543..7d48d249b 100644
--- a/src/theory/arith/nl/ext/tangent_plane_check.h
+++ b/src/theory/arith/nl/ext/tangent_plane_check.h
@@ -19,7 +19,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -67,6 +67,6 @@ class TangentPlaneCheck
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp
index 214d2a51a..125fbb05a 100644
--- a/src/theory/arith/nl/ext_theory_callback.cpp
+++ b/src/theory/arith/nl/ext_theory_callback.cpp
@@ -17,9 +17,9 @@
 #include "theory/arith/arith_utilities.h"
 #include "theory/uf/equality_engine.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -129,4 +129,4 @@ bool NlExtTheoryCallback::isExtfReduced(int effort,
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/ext_theory_callback.h b/src/theory/arith/nl/ext_theory_callback.h
index a3dc74ec8..c747eef69 100644
--- a/src/theory/arith/nl/ext_theory_callback.h
+++ b/src/theory/arith/nl/ext_theory_callback.h
@@ -18,7 +18,7 @@
 #include "expr/node.h"
 #include "theory/ext_theory.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace eq {
 class EqualityEngine;
@@ -84,6 +84,6 @@ class NlExtTheoryCallback : public ExtTheoryCallback
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H */
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index 7272bb6e3..01f4c6e15 100644
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -25,9 +25,9 @@
 #include "theory/rewriter.h"
 #include "util/iand.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -298,4 +298,4 @@ Node IAndSolver::bitwiseLemma(Node i)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
index 137d430c0..95d9632aa 100644
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -22,7 +22,7 @@
 #include "expr/node.h"
 #include "theory/arith/nl/iand_utils.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 
@@ -132,6 +132,6 @@ class IAndSolver
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__ARITH__IAND_SOLVER_H */
diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp
index cb3a03aed..cd96021b0 100644
--- a/src/theory/arith/nl/iand_utils.cpp
+++ b/src/theory/arith/nl/iand_utils.cpp
@@ -21,7 +21,7 @@
 #include "theory/arith/nl/nl_model.h"
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -276,4 +276,4 @@ Node IAndUtils::twoToKMinusOne(unsigned k) const
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/iand_utils.h b/src/theory/arith/nl/iand_utils.h
index a84fcf978..da5f8f04f 100644
--- a/src/theory/arith/nl/iand_utils.h
+++ b/src/theory/arith/nl/iand_utils.h
@@ -20,7 +20,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -169,6 +169,6 @@ class IAndUtils
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__ARITH__IAND_TABLE_H */
diff --git a/src/theory/arith/nl/icp/candidate.cpp b/src/theory/arith/nl/icp/candidate.cpp
index df894ee12..87d823018 100644
--- a/src/theory/arith/nl/icp/candidate.cpp
+++ b/src/theory/arith/nl/icp/candidate.cpp
@@ -23,7 +23,7 @@
 #include "theory/arith/nl/icp/intersection.h"
 #include "theory/arith/nl/poly_conversion.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -115,6 +115,6 @@ std::ostream& operator<<(std::ostream& os, const Candidate& c)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/icp/candidate.h b/src/theory/arith/nl/icp/candidate.h
index 5d8c2b2d0..d4ad11fcf 100644
--- a/src/theory/arith/nl/icp/candidate.h
+++ b/src/theory/arith/nl/icp/candidate.h
@@ -23,7 +23,7 @@
 #include "expr/node.h"
 #include "theory/arith/nl/icp/intersection.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -78,7 +78,7 @@ std::ostream& operator<<(std::ostream& os, const Candidate& c);
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
 
diff --git a/src/theory/arith/nl/icp/contraction_origins.cpp b/src/theory/arith/nl/icp/contraction_origins.cpp
index a076dbdb0..c0b0cb768 100644
--- a/src/theory/arith/nl/icp/contraction_origins.cpp
+++ b/src/theory/arith/nl/icp/contraction_origins.cpp
@@ -14,7 +14,7 @@
 
 #include "theory/arith/nl/icp/contraction_origins.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -117,4 +117,4 @@ inline std::ostream& operator<<(std::ostream& os,
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/icp/contraction_origins.h b/src/theory/arith/nl/icp/contraction_origins.h
index bef6b2848..0f22b5463 100644
--- a/src/theory/arith/nl/icp/contraction_origins.h
+++ b/src/theory/arith/nl/icp/contraction_origins.h
@@ -20,7 +20,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -99,6 +99,6 @@ std::ostream& operator<<(std::ostream& os, const ContractionOriginManager& com);
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp
index 5b505b070..e09264a25 100644
--- a/src/theory/arith/nl/icp/icp_solver.cpp
+++ b/src/theory/arith/nl/icp/icp_solver.cpp
@@ -26,7 +26,7 @@
 #include "theory/rewriter.h"
 #include "util/poly_util.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -384,4 +384,4 @@ void ICPSolver::check()
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h
index 85b2e86c6..56ec03706 100644
--- a/src/theory/arith/nl/icp/icp_solver.h
+++ b/src/theory/arith/nl/icp/icp_solver.h
@@ -28,7 +28,7 @@
 #include "theory/arith/nl/icp/intersection.h"
 #include "theory/arith/nl/poly_conversion.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 
@@ -153,6 +153,6 @@ class ICPSolver
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/icp/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp
index 3dc0ca815..6cdba297c 100644
--- a/src/theory/arith/nl/icp/intersection.cpp
+++ b/src/theory/arith/nl/icp/intersection.cpp
@@ -24,7 +24,7 @@
 #include "base/output.h"
 #include "theory/arith/nl/poly_conversion.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -221,6 +221,6 @@ PropagationResult intersect_interval_with(poly::Interval& cur,
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h
index 1670a8f68..c453f8314 100644
--- a/src/theory/arith/nl/icp/intersection.h
+++ b/src/theory/arith/nl/icp/intersection.h
@@ -25,7 +25,7 @@ namespace poly {
   class Interval;
 }
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -77,7 +77,7 @@ PropagationResult intersect_interval_with(poly::Interval& cur,
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
 
diff --git a/src/theory/arith/nl/icp/interval.h b/src/theory/arith/nl/icp/interval.h
index ff4bbfcac..8acbfec05 100644
--- a/src/theory/arith/nl/icp/interval.h
+++ b/src/theory/arith/nl/icp/interval.h
@@ -22,7 +22,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -58,7 +58,7 @@ inline std::ostream& operator<<(std::ostream& os, const Interval& i)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
 
diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp
index d7785dbc9..f3c2d70c8 100644
--- a/src/theory/arith/nl/nl_lemma_utils.cpp
+++ b/src/theory/arith/nl/nl_lemma_utils.cpp
@@ -17,7 +17,7 @@
 #include "theory/arith/nl/nl_model.h"
 #include "theory/arith/nl/nonlinear_extension.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -78,4 +78,4 @@ Node ArgTrie::add(Node d, const std::vector<Node>& args)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h
index 6f3ef077a..71d86b08a 100644
--- a/src/theory/arith/nl/nl_lemma_utils.h
+++ b/src/theory/arith/nl/nl_lemma_utils.h
@@ -21,7 +21,7 @@
 #include "expr/node.h"
 #include "theory/theory_inference.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -144,6 +144,6 @@ class ArgTrie
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__ARITH__NL_LEMMA_UTILS_H */
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index 5467c64ce..f7edefff7 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -24,9 +24,9 @@
 #include "theory/theory_model.h"
 #include "theory/rewriter.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -1342,4 +1342,4 @@ void NlModel::getModelValueRepair(
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h
index cd52cb159..b2c435098 100644
--- a/src/theory/arith/nl/nl_model.h
+++ b/src/theory/arith/nl/nl_model.h
@@ -22,7 +22,7 @@
 #include "expr/kind.h"
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 namespace context {
 class Context;
@@ -329,6 +329,6 @@ class NlModel
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 781fb0c71..ff1962629 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -27,9 +27,9 @@
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -621,4 +621,4 @@ void NonlinearExtension::runStrategy(Theory::Effort effort,
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index bc8f48c26..b6fb53651 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -41,7 +41,7 @@
 #include "theory/theory.h"
 #include "util/result.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace eq {
   class EqualityEngine;
@@ -296,6 +296,6 @@ class NonlinearExtension
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */
diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp
index 0dd7cc070..5738dccfc 100644
--- a/src/theory/arith/nl/poly_conversion.cpp
+++ b/src/theory/arith/nl/poly_conversion.cpp
@@ -23,12 +23,12 @@
 #include "theory/arith/bound_inference.h"
 #include "util/poly_util.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
 
-poly::Variable VariableMapper::operator()(const CVC4::Node& n)
+poly::Variable VariableMapper::operator()(const CVC5::Node& n)
 {
   auto it = mVarCVCpoly.find(n);
   if (it == mVarCVCpoly.end())
@@ -54,7 +54,7 @@ poly::Variable VariableMapper::operator()(const CVC4::Node& n)
   return it->second;
 }
 
-CVC4::Node VariableMapper::operator()(const poly::Variable& n)
+CVC5::Node VariableMapper::operator()(const poly::Variable& n)
 {
   auto it = mVarpolyCVC.find(n);
   Assert(it != mVarpolyCVC.end())
@@ -62,7 +62,7 @@ CVC4::Node VariableMapper::operator()(const poly::Variable& n)
   return it->second;
 }
 
-CVC4::Node as_cvc_upolynomial(const poly::UPolynomial& p, const CVC4::Node& var)
+CVC5::Node as_cvc_upolynomial(const poly::UPolynomial& p, const CVC5::Node& var)
 {
   Trace("poly::conversion")
       << "Converting " << p << " over " << var << std::endl;
@@ -87,9 +87,9 @@ CVC4::Node as_cvc_upolynomial(const poly::UPolynomial& p, const CVC4::Node& var)
   return res;
 }
 
-poly::UPolynomial as_poly_upolynomial_impl(const CVC4::Node& n,
+poly::UPolynomial as_poly_upolynomial_impl(const CVC5::Node& n,
                                            poly::Integer& denominator,
-                                           const CVC4::Node& var)
+                                           const CVC5::Node& var)
 {
   denominator = poly::Integer(1);
   if (n.isVar())
@@ -140,14 +140,14 @@ poly::UPolynomial as_poly_upolynomial_impl(const CVC4::Node& n,
   return poly::UPolynomial();
 }
 
-poly::UPolynomial as_poly_upolynomial(const CVC4::Node& n,
-                                      const CVC4::Node& var)
+poly::UPolynomial as_poly_upolynomial(const CVC5::Node& n,
+                                      const CVC5::Node& var)
 {
   poly::Integer denom;
   return as_poly_upolynomial_impl(n, denom, var);
 }
 
-poly::Polynomial as_poly_polynomial_impl(const CVC4::Node& n,
+poly::Polynomial as_poly_polynomial_impl(const CVC5::Node& n,
                                          poly::Integer& denominator,
                                          VariableMapper& vm)
 {
@@ -195,12 +195,12 @@ poly::Polynomial as_poly_polynomial_impl(const CVC4::Node& n,
   }
   return poly::Polynomial();
 }
-poly::Polynomial as_poly_polynomial(const CVC4::Node& n, VariableMapper& vm)
+poly::Polynomial as_poly_polynomial(const CVC5::Node& n, VariableMapper& vm)
 {
   poly::Integer denom;
   return as_poly_polynomial_impl(n, denom, vm);
 }
-poly::Polynomial as_poly_polynomial(const CVC4::Node& n,
+poly::Polynomial as_poly_polynomial(const CVC5::Node& n,
                                     VariableMapper& vm,
                                     poly::Rational& denominator)
 {
@@ -257,7 +257,7 @@ void collect_monomials(const lp_polynomial_context_t* ctx,
 }
 }  // namespace
 
-CVC4::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm)
+CVC5::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm)
 {
   CollectMonomialData cmd(vm);
   // Do the actual conversion
@@ -274,7 +274,7 @@ CVC4::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm)
   return cmd.d_nm->mkNode(Kind::PLUS, cmd.d_terms);
 }
 
-poly::SignCondition normalize_kind(CVC4::Kind kind,
+poly::SignCondition normalize_kind(CVC5::Kind kind,
                                    bool negated,
                                    poly::Polynomial& lhs)
 {
@@ -803,6 +803,6 @@ poly::IntervalAssignment getBounds(VariableMapper& vm, const BoundInference& bi)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h
index 47a66d5f1..9adc9a996 100644
--- a/src/theory/arith/nl/poly_conversion.h
+++ b/src/theory/arith/nl/poly_conversion.h
@@ -30,7 +30,7 @@
 #include "expr/node.h"
 #include "util/real_algebraic_number.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 
@@ -42,23 +42,23 @@ namespace nl {
 struct VariableMapper
 {
   /** A mapping from CVC4 variables to poly variables. */
-  std::map<CVC4::Node, poly::Variable> mVarCVCpoly;
+  std::map<CVC5::Node, poly::Variable> mVarCVCpoly;
   /** A mapping from poly variables to CVC4 variables. */
-  std::map<poly::Variable, CVC4::Node> mVarpolyCVC;
+  std::map<poly::Variable, CVC5::Node> mVarpolyCVC;
 
   /** Retrieves the according poly variable. */
-  poly::Variable operator()(const CVC4::Node& n);
+  poly::Variable operator()(const CVC5::Node& n);
   /** Retrieves the according CVC4 variable. */
-  CVC4::Node operator()(const poly::Variable& n);
+  CVC5::Node operator()(const poly::Variable& n);
 };
 
-/** Convert a poly univariate polynomial to a CVC4::Node. */
-CVC4::Node as_cvc_upolynomial(const poly::UPolynomial& p,
-                              const CVC4::Node& var);
+/** Convert a poly univariate polynomial to a CVC5::Node. */
+CVC5::Node as_cvc_upolynomial(const poly::UPolynomial& p,
+                              const CVC5::Node& var);
 
-/** Convert a CVC4::Node to a poly univariate polynomial. */
-poly::UPolynomial as_poly_upolynomial(const CVC4::Node& n,
-                                      const CVC4::Node& var);
+/** Convert a CVC5::Node to a poly univariate polynomial. */
+poly::UPolynomial as_poly_upolynomial(const CVC5::Node& n,
+                                      const CVC5::Node& var);
 
 /**
  * Constructs a polynomial from the given node.
@@ -73,8 +73,8 @@ poly::UPolynomial as_poly_upolynomial(const CVC4::Node& n,
  * in the context of ICP) the second overload provides the denominator in the
  * third argument.
  */
-poly::Polynomial as_poly_polynomial(const CVC4::Node& n, VariableMapper& vm);
-poly::Polynomial as_poly_polynomial(const CVC4::Node& n,
+poly::Polynomial as_poly_polynomial(const CVC5::Node& n, VariableMapper& vm);
+poly::Polynomial as_poly_polynomial(const CVC5::Node& n,
                                     VariableMapper& vm,
                                     poly::Rational& denominator);
 
@@ -87,7 +87,7 @@ poly::Polynomial as_poly_polynomial(const CVC4::Node& n,
  * multiplications with one or use NONLINEAR_MULT where regular MULT may be
  * sufficient), so it may be sensible to rewrite it afterwards.
  */
-CVC4::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm);
+CVC5::Node as_cvc_polynomial(const poly::Polynomial& p, VariableMapper& vm);
 
 /**
  * Constructs a constraints (a polynomial and a sign condition) from the given
@@ -164,7 +164,7 @@ poly::IntervalAssignment getBounds(VariableMapper& vm, const BoundInference& bi)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
 
diff --git a/src/theory/arith/nl/stats.cpp b/src/theory/arith/nl/stats.cpp
index c707dd9bc..92cebc8fc 100644
--- a/src/theory/arith/nl/stats.cpp
+++ b/src/theory/arith/nl/stats.cpp
@@ -16,7 +16,7 @@
 
 #include "smt/smt_statistics_registry.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -38,4 +38,4 @@ NlStats::~NlStats()
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h
index 94e1882b3..66157d0a3 100644
--- a/src/theory/arith/nl/stats.h
+++ b/src/theory/arith/nl/stats.h
@@ -19,7 +19,7 @@
 
 #include "util/statistics_registry.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -44,6 +44,6 @@ class NlStats
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__ARITH__NL__STATS_H */
diff --git a/src/theory/arith/nl/strategy.cpp b/src/theory/arith/nl/strategy.cpp
index 5d6eeea9e..af23f67f9 100644
--- a/src/theory/arith/nl/strategy.cpp
+++ b/src/theory/arith/nl/strategy.cpp
@@ -19,7 +19,7 @@
 #include "base/check.h"
 #include "options/arith_options.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -173,4 +173,4 @@ StepGenerator Strategy::getStrategy()
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h
index 3540f9ad1..9caf6322b 100644
--- a/src/theory/arith/nl/strategy.h
+++ b/src/theory/arith/nl/strategy.h
@@ -18,7 +18,7 @@
 #include <iosfwd>
 #include <vector>
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -173,6 +173,6 @@ class Strategy
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__ARITH__NL__STRATEGY_H */
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index 8b6f4484d..05849a579 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -28,7 +28,7 @@
 #include "theory/arith/nl/transcendental/transcendental_state.h"
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -276,4 +276,4 @@ std::pair<Node, Node> ExponentialSolver::getSecantBounds(TNode e,
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h
index 484174d5f..8bd00c456 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.h
+++ b/src/theory/arith/nl/transcendental/exponential_solver.h
@@ -19,7 +19,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -108,6 +108,6 @@ class ExponentialSolver
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp
index 223db8355..fe071c36a 100644
--- a/src/theory/arith/nl/transcendental/proof_checker.cpp
+++ b/src/theory/arith/nl/transcendental/proof_checker.cpp
@@ -19,9 +19,9 @@
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 #include "theory/rewriter.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -402,4 +402,4 @@ Node TranscendentalProofRuleChecker::checkInternal(
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/transcendental/proof_checker.h b/src/theory/arith/nl/transcendental/proof_checker.h
index b00c1811c..2a6837590 100644
--- a/src/theory/arith/nl/transcendental/proof_checker.h
+++ b/src/theory/arith/nl/transcendental/proof_checker.h
@@ -21,7 +21,7 @@
 #include "expr/proof_checker.h"
 #include "expr/proof_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -53,6 +53,6 @@ class TranscendentalProofRuleChecker : public ProofRuleChecker
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 528e0bea2..052b6c056 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -28,7 +28,7 @@
 #include "theory/arith/nl/transcendental/transcendental_state.h"
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -484,4 +484,4 @@ std::pair<Node, Node> SineSolver::getSecantBounds(TNode e,
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h
index c628559fc..c20c50f6d 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.h
+++ b/src/theory/arith/nl/transcendental/sine_solver.h
@@ -20,7 +20,7 @@
 #include "expr/node.h"
 #include "theory/arith/nl/transcendental/transcendental_state.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -175,6 +175,6 @@ class SineSolver
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp
index ced202308..f2817344a 100644
--- a/src/theory/arith/nl/transcendental/taylor_generator.cpp
+++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp
@@ -18,7 +18,7 @@
 #include "theory/arith/nl/nl_model.h"
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -243,4 +243,4 @@ std::pair<Node, Node> TaylorGenerator::getTfModelBounds(Node tf,
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h
index 7cb03cd7c..b13be57f0 100644
--- a/src/theory/arith/nl/transcendental/taylor_generator.h
+++ b/src/theory/arith/nl/transcendental/taylor_generator.h
@@ -17,7 +17,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -118,6 +118,6 @@ class TaylorGenerator
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index f236b472a..bedfe4d3b 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -27,9 +27,9 @@
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 #include "theory/rewriter.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -438,4 +438,4 @@ int TranscendentalSolver::regionToConcavity(Kind k, int region)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h
index 290e74322..e22bf3e64 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.h
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.h
@@ -22,7 +22,7 @@
 #include "theory/arith/nl/transcendental/sine_solver.h"
 #include "theory/arith/nl/transcendental/transcendental_state.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 
@@ -200,6 +200,6 @@ class TranscendentalSolver
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index 593354794..6ab136d39 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -21,7 +21,7 @@
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 #include "theory/rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -437,4 +437,4 @@ void TranscendentalState::doSecantLemmas(const std::pair<Node, Node>& bounds,
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h
index cd5466e89..21a60e038 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.h
+++ b/src/theory/arith/nl/transcendental/transcendental_state.h
@@ -21,7 +21,7 @@
 #include "theory/arith/nl/transcendental/proof_checker.h"
 #include "theory/arith/nl/transcendental/taylor_generator.h"
 
-namespace CVC4 {
+namespace CVC5 {
 class CDProof;
 namespace theory {
 namespace arith {
@@ -278,6 +278,6 @@ struct TranscendentalState
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H */