Rename namespace CVC4 to CVC5. (#6249)

72 files changed, 204 insertions, 200 deletions

diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp
index 2c82b98e9..4f6cadde4 100644
--- a/src/util/abstract_value.cpp
+++ b/src/util/abstract_value.cpp
@@ -24,7 +24,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 
 std::ostream& operator<<(std::ostream& out, const AbstractValue& val) {
   return out << "@" << val.getIndex();
@@ -38,4 +38,4 @@ AbstractValue::AbstractValue(Integer index) : d_index(index)
                       index.toString().c_str());
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h
index 5d28d355a..ddd1018a2 100644
--- a/src/util/abstract_value.h
+++ b/src/util/abstract_value.h
@@ -22,7 +22,7 @@
 
 #include "util/integer.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class AbstractValue
 {
@@ -61,4 +61,4 @@ struct AbstractValueHashFunction
   }
 }; /* struct AbstractValueHashFunction */
 
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/util/bin_heap.h b/src/util/bin_heap.h
index c51600122..40f2da045 100644
--- a/src/util/bin_heap.h
+++ b/src/util/bin_heap.h
@@ -29,7 +29,7 @@
 #include "base/check.h"
 #include "base/exception.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * BinaryHeap that orders its elements greatest-first (i.e., in the opposite
@@ -363,6 +363,6 @@ private:
 template <class Elem, class CmpFcn>
 const size_t BinaryHeap<Elem,CmpFcn>::MAX_SIZE = (std::numeric_limits<size_t>::max()-2)/2;
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__BIN_HEAP_H */
diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
index 3d907150d..85b373886 100644
--- a/src/util/bitvector.cpp
+++ b/src/util/bitvector.cpp
@@ -20,7 +20,7 @@
 
 #include "base/exception.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 unsigned BitVector::getSize() const { return d_size; }
 
@@ -375,4 +375,4 @@ BitVector BitVector::mkMaxSigned(unsigned size)
   return ~BitVector::mkMinSigned(size);
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index c5a690c03..fbb91b8e3 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -25,7 +25,7 @@
 #include "base/exception.h"
 #include "util/integer.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class BitVector
 {
@@ -442,6 +442,6 @@ inline std::ostream& operator<<(std::ostream& os, const IntToBitVector& bv)
   return os << "[" << bv.d_size << "]";
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__BITVECTOR_H */
diff --git a/src/util/bool.h b/src/util/bool.h
index 0dd179d6a..d1f57fcd4 100644
--- a/src/util/bool.h
+++ b/src/util/bool.h
@@ -19,7 +19,7 @@
 #ifndef CVC4__BOOL_H
 #define CVC4__BOOL_H
 
-namespace CVC4 {
+namespace CVC5 {
 
 struct BoolHashFunction {
   inline size_t operator()(bool b) const {
@@ -27,6 +27,6 @@ struct BoolHashFunction {
   }
 };/* struct BoolHashFunction */
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__BOOL_H */
diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
index 3ab44d6f8..027c3d2db 100644
--- a/src/util/cardinality.cpp
+++ b/src/util/cardinality.cpp
@@ -22,7 +22,7 @@
 #include "base/check.h"
 #include "base/exception.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 const Integer Cardinality::s_unknownCard(0);
 const Integer Cardinality::s_intCard(-1);
@@ -263,4 +263,4 @@ std::ostream& operator<<(std::ostream& out, const Cardinality& c) {
   return out;
 }
 
-} /* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index 6c48b44a8..2ab2fdd63 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -24,7 +24,7 @@
 
 #include "util/integer.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * Representation for a Beth number, used only to construct
@@ -225,6 +225,6 @@ std::ostream& operator<<(std::ostream& out, CardinalityBeth b);
 /** Print a cardinality in a human-readable fashion. */
 std::ostream& operator<<(std::ostream& out, const Cardinality& c);
 
-} /* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__CARDINALITY_H */
diff --git a/src/util/dense_map.h b/src/util/dense_map.h
index 7a3421281..e6fed6916 100644
--- a/src/util/dense_map.h
+++ b/src/util/dense_map.h
@@ -35,8 +35,7 @@
 #include "base/check.h"
 #include "util/index.h"
 
-
-namespace CVC4 {
+namespace CVC5 {
 
 template <class T>
 class DenseMap {
@@ -339,4 +338,4 @@ public:
   void pop_back() { d_map.pop_back(); }
 }; /* class DenseMultiset */
 
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/util/divisible.cpp b/src/util/divisible.cpp
index b3c823e06..45b1f6c27 100644
--- a/src/util/divisible.cpp
+++ b/src/util/divisible.cpp
@@ -22,10 +22,10 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 
 Divisible::Divisible(const Integer& n) : k(n) {
   PrettyCheckArgument(n > 0, n, "Divisible predicate must be constructed over positive N");
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/util/divisible.h b/src/util/divisible.h
index 2de81c52b..5b3506ee8 100644
--- a/src/util/divisible.h
+++ b/src/util/divisible.h
@@ -26,7 +26,7 @@
 
 #include "util/integer.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * The structure representing the divisibility-by-k predicate.
@@ -61,6 +61,6 @@ inline std::ostream& operator <<(std::ostream& os, const Divisible& d) {
   return os << "divisible-by-" << d.k;
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__DIVISIBLE_H */
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index 26bdb65f4..be5f6a496 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -28,7 +28,7 @@
 
 /* -------------------------------------------------------------------------- */
 
-namespace CVC4 {
+namespace CVC5 {
 
 /* -------------------------------------------------------------------------- */
 
@@ -512,4 +512,4 @@ std::ostream& operator<<(std::ostream& os, const FloatingPointConvertSort& fpcs)
   return os << "(_ to_fp " << fpcs.getSize().exponentWidth() << " "
             << fpcs.getSize().significandWidth() << ")";
 }
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h
index b6c1bfb53..060d1de99 100644
--- a/src/util/floatingpoint.h
+++ b/src/util/floatingpoint.h
@@ -29,7 +29,7 @@
 
 /* -------------------------------------------------------------------------- */
 
-namespace CVC4 {
+namespace CVC5 {
 
 /* -------------------------------------------------------------------------- */
 
@@ -514,7 +514,7 @@ struct FloatingPointToBVHashFunction
 {
   inline size_t operator()(const FloatingPointToBV& fptbv) const
   {
-    UnsignedHashFunction< ::CVC4::BitVectorSize> f;
+    UnsignedHashFunction< ::CVC5::BitVectorSize> f;
     return (key ^ 0x46504256) ^ f(fptbv.d_bv_size);
   }
 }; /* struct FloatingPointToBVHashFunction */
@@ -533,6 +533,6 @@ std::ostream& operator<<(std::ostream& os, const FloatingPointSize& fps);
 std::ostream& operator<<(std::ostream& os,
                          const FloatingPointConvertSort& fpcs);
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__FLOATINGPOINT_H */
diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp
index 1d40292f7..efd3e2399 100644
--- a/src/util/floatingpoint_literal_symfpu.cpp
+++ b/src/util/floatingpoint_literal_symfpu.cpp
@@ -39,9 +39,9 @@ namespace symfpu {
 
 #define CVC4_LIT_ITE_DFN(T)                                            \
   template <>                                                          \
-  struct ite<::CVC4::symfpuLiteral::CVC4Prop, T>                       \
+  struct ite<::CVC5::symfpuLiteral::CVC4Prop, T>                       \
   {                                                                    \
-    static const T& iteOp(const ::CVC4::symfpuLiteral::CVC4Prop& cond, \
+    static const T& iteOp(const ::CVC5::symfpuLiteral::CVC4Prop& cond, \
                           const T& l,                                  \
                           const T& r)                                  \
     {                                                                  \
@@ -49,10 +49,10 @@ namespace symfpu {
     }                                                                  \
   }
 
-CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::rm);
-CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::prop);
-CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::sbv);
-CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv);
+CVC4_LIT_ITE_DFN(::CVC5::symfpuLiteral::traits::rm);
+CVC4_LIT_ITE_DFN(::CVC5::symfpuLiteral::traits::prop);
+CVC4_LIT_ITE_DFN(::CVC5::symfpuLiteral::traits::sbv);
+CVC4_LIT_ITE_DFN(::CVC5::symfpuLiteral::traits::ubv);
 
 #undef CVC4_LIT_ITE_DFN
 }  // namespace symfpu
@@ -60,7 +60,7 @@ CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv);
 
 /* -------------------------------------------------------------------------- */
 
-namespace CVC4 {
+namespace CVC5 {
 
 uint32_t FloatingPointLiteral::getUnpackedExponentWidth(FloatingPointSize& size)
 {
@@ -881,11 +881,11 @@ wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract(
 template class wrappedBitVector<true>;
 template class wrappedBitVector<false>;
 
-traits::rm traits::RNE(void) { return ::CVC4::ROUND_NEAREST_TIES_TO_EVEN; };
-traits::rm traits::RNA(void) { return ::CVC4::ROUND_NEAREST_TIES_TO_AWAY; };
-traits::rm traits::RTP(void) { return ::CVC4::ROUND_TOWARD_POSITIVE; };
-traits::rm traits::RTN(void) { return ::CVC4::ROUND_TOWARD_NEGATIVE; };
-traits::rm traits::RTZ(void) { return ::CVC4::ROUND_TOWARD_ZERO; };
+traits::rm traits::RNE(void) { return ::CVC5::ROUND_NEAREST_TIES_TO_EVEN; };
+traits::rm traits::RNA(void) { return ::CVC5::ROUND_NEAREST_TIES_TO_AWAY; };
+traits::rm traits::RTP(void) { return ::CVC5::ROUND_TOWARD_POSITIVE; };
+traits::rm traits::RTN(void) { return ::CVC5::ROUND_TOWARD_NEGATIVE; };
+traits::rm traits::RTZ(void) { return ::CVC5::ROUND_TOWARD_ZERO; };
 // This is a literal back-end so props are actually bools
 // so these can be handled in the same way as the internal assertions above
 
@@ -906,4 +906,4 @@ void traits::invariant(const traits::prop& p)
 }
 }  // namespace symfpuLiteral
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h.in
index 8857728ce..d01bf6a9d 100644
--- a/src/util/floatingpoint_literal_symfpu.h.in
+++ b/src/util/floatingpoint_literal_symfpu.h.in
@@ -30,7 +30,7 @@
 
 /* -------------------------------------------------------------------------- */
 
-namespace CVC4 {
+namespace CVC5 {
 
 class FloatingPointSize;
 class FloatingPointLiteral;
@@ -56,8 +56,8 @@ class wrappedBitVector;
 
 using CVC4BitWidth = uint32_t;
 using CVC4Prop = bool;
-using CVC4RM = ::CVC4::RoundingMode;
-using CVC4FPSize = ::CVC4::FloatingPointSize;
+using CVC4RM = ::CVC5::RoundingMode;
+using CVC4FPSize = ::CVC5::FloatingPointSize;
 using CVC4UnsignedBitVector = wrappedBitVector<false>;
 using CVC4SignedBitVector = wrappedBitVector<true>;
 
@@ -106,7 +106,7 @@ struct signedToLiteralType<false>
 };
 
 /**
- * This extends the interface for CVC4::BitVector for compatibility with symFPU.
+ * This extends the interface for CVC5::BitVector for compatibility with symFPU.
  * The template parameter distinguishes signed and unsigned bit-vectors, a
  * distinction symfpu uses.
  */
@@ -159,7 +159,7 @@ class wrappedBitVector : public BitVector
   /**
    * Inherited but ...
    * *sigh* if we use the inherited version then it will return a
-   * CVC4::BitVector which can be converted back to a
+   * CVC5::BitVector which can be converted back to a
    * wrappedBitVector<isSigned> but isn't done automatically when working
    * out types for templates instantiation.  ITE is a particular
    * problem as expressions and constants no longer derive the
@@ -502,6 +502,6 @@ class FloatingPointLiteral
 
 /* -------------------------------------------------------------------------- */
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/util/floatingpoint_size.cpp b/src/util/floatingpoint_size.cpp
index 9b14db699..78558ab27 100644
--- a/src/util/floatingpoint_size.cpp
+++ b/src/util/floatingpoint_size.cpp
@@ -15,7 +15,7 @@
 
 #include "base/check.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 FloatingPointSize::FloatingPointSize(uint32_t exp_size, uint32_t sig_size)
     : d_exp_size(exp_size), d_sig_size(sig_size)
@@ -31,4 +31,4 @@ FloatingPointSize::FloatingPointSize(const FloatingPointSize& old)
   Assert(validSignificandSize(d_sig_size));
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/util/floatingpoint_size.h b/src/util/floatingpoint_size.h
index be00e0987..ed5dccc4f 100644
--- a/src/util/floatingpoint_size.h
+++ b/src/util/floatingpoint_size.h
@@ -16,7 +16,7 @@
 #ifndef CVC4__FLOATINGPOINT_SIZE_H
 #define CVC4__FLOATINGPOINT_SIZE_H
 
-namespace CVC4 {
+namespace CVC5 {
 
 // Inline these!
 inline bool validExponentSize(uint32_t e) { return e >= 2; }
@@ -92,6 +92,6 @@ struct FloatingPointSizeHashFunction
                   | t.significandWidth());
   }
 }; /* struct FloatingPointSizeHashFunction */
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h
index bf13669d3..0ecc6485d 100644
--- a/src/util/gmp_util.h
+++ b/src/util/gmp_util.h
@@ -22,7 +22,7 @@
 
 #include <gmpxx.h>
 
-namespace CVC4 {
+namespace CVC5 {
 
 /** Hashes the gmp integer primitive in a word by word fashion. */
 inline size_t gmpz_hash(const mpz_t toHash) {
@@ -35,6 +35,6 @@ inline size_t gmpz_hash(const mpz_t toHash) {
   return hash;
 }/* gmpz_hash() */
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__GMP_UTIL_H */
diff --git a/src/util/hash.h b/src/util/hash.h
index 8adb4b473..066e01aad 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -38,7 +38,7 @@ struct hash<uint64_t> {
 
 }/* std namespace */
 
-namespace CVC4 {
+namespace CVC5 {
 
 namespace fnv1a {
 
@@ -64,6 +64,6 @@ struct PairHashFunction {
   }
 };/* struct PairHashFunction */
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__HASH_H */
diff --git a/src/util/iand.h b/src/util/iand.h
index e5f1a5af7..a50c4aeb7 100644
--- a/src/util/iand.h
+++ b/src/util/iand.h
@@ -22,7 +22,7 @@
 #include "base/exception.h"
 #include "util/integer.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 struct IntAnd
 {
@@ -41,6 +41,6 @@ inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia)
   return os << "[" << ia.d_size << "]";
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__IAND_H */
diff --git a/src/util/index.cpp b/src/util/index.cpp
index f3b3df29d..7c9f3c57f 100644
--- a/src/util/index.cpp
+++ b/src/util/index.cpp
@@ -19,7 +19,7 @@
 
 #include <limits>
 
-namespace CVC4 {
+namespace CVC5 {
 
 static_assert(sizeof(Index) <= sizeof(size_t),
               "Index cannot be larger than size_t");
@@ -34,4 +34,4 @@ static_assert(!std::numeric_limits<Index>::is_signed,
  * (Limited testing suggests a ~1/16 of running time.) Interestingly,
  * uint_fast32_t also has a sizeof == 8 on x86_64.
  */
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/util/index.h b/src/util/index.h
index 6a050f4f9..1fa881eb6 100644
--- a/src/util/index.h
+++ b/src/util/index.h
@@ -19,11 +19,11 @@
 #ifndef CVC4__INDEX_H
 #define CVC4__INDEX_H
 
-namespace CVC4 {
+namespace CVC5 {
 
 /** Index is a standardized unsigned integer used for efficient indexing. */
 using Index = uint32_t;
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__INDEX_H */
diff --git a/src/util/indexed_root_predicate.h b/src/util/indexed_root_predicate.h
index 3c36a6a97..b201630c0 100644
--- a/src/util/indexed_root_predicate.h
+++ b/src/util/indexed_root_predicate.h
@@ -19,7 +19,7 @@
 #ifndef CVC4__UTIL__INDEXED_ROOT_PREDICATE_H
 #define CVC4__UTIL__INDEXED_ROOT_PREDICATE_H
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * The structure representing the index of a root predicate.
@@ -69,6 +69,6 @@ struct IndexedRootPredicateHashFunction
   }
 }; /* struct IndexedRootPredicateHashFunction */
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
\ No newline at end of file
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index a4035165e..0f02f03e5 100644
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -28,7 +28,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 
 signed int Integer::s_fastSignedIntMin = -(1 << 29);
 signed int Integer::s_fastSignedIntMax = (1 << 29) - 1;
@@ -568,4 +568,4 @@ std::ostream& operator<<(std::ostream& os, const Integer& n)
 {
   return os << n.toString();
 }
-} /* namespace CVC4 */
+} // namespace CVC5
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index db1e5068f..7d7b002f2 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -33,13 +33,13 @@
 #include "base/exception.h"
 #include "cvc4_export.h"  // remove when Cvc language support is removed
 
-namespace CVC4 {
+namespace CVC5 {
 
 class Rational;
 
 class CVC4_EXPORT Integer
 {
-  friend class CVC4::Rational;
+  friend class CVC5::Rational;
 
  public:
   /**
@@ -380,11 +380,11 @@ class CVC4_EXPORT Integer
 
 struct IntegerHashFunction
 {
-  size_t operator()(const CVC4::Integer& i) const { return i.hash(); }
+  size_t operator()(const CVC5::Integer& i) const { return i.hash(); }
 }; /* struct IntegerHashFunction */
 
 std::ostream& operator<<(std::ostream& os, const Integer& n);
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__INTEGER_H */
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index 89f6dc308..d1e0d7108 100644
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -31,7 +31,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 
 Integer::Integer(const char* s, unsigned base)
   : d_value(s, base)
@@ -483,4 +483,4 @@ const Integer& Integer::max(const Integer& a, const Integer& b)
   return (a >= b) ? a : b;
 }
 
-} /* namespace CVC4 */
+} // namespace CVC5
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 616408b42..fa206d08f 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -27,13 +27,13 @@
 
 #include "cvc4_export.h"  // remove when Cvc language support is removed
 
-namespace CVC4 {
+namespace CVC5 {
 
 class Rational;
 
 class CVC4_EXPORT Integer
 {
-  friend class CVC4::Rational;
+  friend class CVC5::Rational;
 
  public:
   /**
@@ -330,7 +330,7 @@ class CVC4_EXPORT Integer
 
 struct IntegerHashFunction
 {
-  inline size_t operator()(const CVC4::Integer& i) const { return i.hash(); }
+  inline size_t operator()(const CVC5::Integer& i) const { return i.hash(); }
 }; /* struct IntegerHashFunction */
 
 inline std::ostream& operator<<(std::ostream& os, const Integer& n)
@@ -338,6 +338,6 @@ inline std::ostream& operator<<(std::ostream& os, const Integer& n)
   return os << n.toString();
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__INTEGER_H */
diff --git a/src/util/maybe.h b/src/util/maybe.h
index a74a42a17..35c0efd68 100644
--- a/src/util/maybe.h
+++ b/src/util/maybe.h
@@ -31,7 +31,7 @@
 
 #include "base/exception.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 template <class T>
 class Maybe
@@ -84,6 +84,6 @@ inline std::ostream& operator<<(std::ostream& out, const Maybe<T>& m){
   return out;
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__UTIL__MAYBE_H */
diff --git a/src/util/ostream_util.cpp b/src/util/ostream_util.cpp
index dd9d3bf92..37fa0d892 100644
--- a/src/util/ostream_util.cpp
+++ b/src/util/ostream_util.cpp
@@ -17,7 +17,7 @@
 
 #include <ostream>
 
-namespace CVC4 {
+namespace CVC5 {
 
 StreamFormatScope::StreamFormatScope(std::ostream& out)
     : d_out(out), d_format_flags(out.flags()), d_precision(out.precision())
@@ -30,4 +30,4 @@ StreamFormatScope::~StreamFormatScope()
   d_out.flags(d_format_flags);
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/util/ostream_util.h b/src/util/ostream_util.h
index 1f70e33ad..c5e1e2797 100644
--- a/src/util/ostream_util.h
+++ b/src/util/ostream_util.h
@@ -22,7 +22,7 @@
 #include <ios>
 #include <iosfwd>
 
-namespace CVC4 {
+namespace CVC5 {
 
 // Saves the formatting of an ostream and restores the previous settings on
 // destruction. Example usage:
@@ -44,6 +44,6 @@ class StreamFormatScope
   std::streamsize d_precision;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__UTIL__OSTREAM_UTIL_H */
diff --git a/src/util/poly_util.cpp b/src/util/poly_util.cpp
index e9f80bf77..9dbb24872 100644
--- a/src/util/poly_util.cpp
+++ b/src/util/poly_util.cpp
@@ -35,7 +35,7 @@
 #include "util/rational.h"
 #include "util/real_algebraic_number.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace poly_utils {
 
 namespace {
@@ -361,6 +361,6 @@ void getVariableInformation(VariableInformation& vi,
 }
 
 }  // namespace poly_utils
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/util/poly_util.h b/src/util/poly_util.h
index 203aec618..efb185932 100644
--- a/src/util/poly_util.h
+++ b/src/util/poly_util.h
@@ -36,7 +36,7 @@
 
 #include <poly/polyxx.h>
 
-namespace CVC4 {
+namespace CVC5 {
 /**
  * Utilities for working with libpoly.
  * This namespace contains various basic conversion routines necessary for the
@@ -49,28 +49,28 @@ namespace CVC4 {
  */
 namespace poly_utils {
 
-/** Converts a poly::Integer to a CVC4::Integer. */
+/** Converts a poly::Integer to a CVC5::Integer. */
 Integer toInteger(const poly::Integer& i);
-/** Converts a poly::Integer to a CVC4::Rational. */
+/** Converts a poly::Integer to a CVC5::Rational. */
 Rational toRational(const poly::Integer& r);
-/** Converts a poly::Rational to a CVC4::Rational. */
+/** Converts a poly::Rational to a CVC5::Rational. */
 Rational toRational(const poly::Rational& r);
-/** Converts a poly::DyadicRational to a CVC4::Rational. */
+/** Converts a poly::DyadicRational to a CVC5::Rational. */
 Rational toRational(const poly::DyadicRational& dr);
 
-/** Converts a poly::Value to a CVC4::Rational (that may be a bit above). */
+/** Converts a poly::Value to a CVC5::Rational (that may be a bit above). */
 Rational toRationalAbove(const poly::Value& v);
-/** Converts a poly::Value to a CVC4::Rational (that may be a bit below). */
+/** Converts a poly::Value to a CVC5::Rational (that may be a bit below). */
 Rational toRationalBelow(const poly::Value& v);
 
-/** Converts a CVC4::Integer to a poly::Integer. */
+/** Converts a CVC5::Integer to a poly::Integer. */
 poly::Integer toInteger(const Integer& i);
-/** Converts a vector of CVC4::Integers to a vector of poly::Integers. */
+/** Converts a vector of CVC5::Integers to a vector of poly::Integers. */
 std::vector<poly::Integer> toInteger(const std::vector<Integer>& vi);
-/** Converts a CVC4::Rational to a poly::Rational. */
+/** Converts a CVC5::Rational to a poly::Rational. */
 poly::Rational toRational(const Rational& r);
 /**
- * Converts a CVC4::Rational to a poly::DyadicRational. If the input is not
+ * Converts a CVC5::Rational to a poly::DyadicRational. If the input is not
  * dyadic, no result is produced.
  */
 Maybe<poly::DyadicRational> toDyadicRational(const Rational& r);
@@ -91,7 +91,7 @@ poly::Rational approximateToDyadic(const poly::Rational& r,
 
 /**
  * Constructs a poly::AlgebraicNumber, allowing for refinement of the
- * CVC4::Rational bounds. As a poly::AlgebraicNumber works on
+ * CVC5::Rational bounds. As a poly::AlgebraicNumber works on
  * poly::DyadicRationals internally, the bounds are iteratively refined using
  * approximateToDyadic until the respective interval is isolating. If the
  * provided rational bounds are already dyadic, the refinement is skipped.
@@ -101,7 +101,7 @@ poly::AlgebraicNumber toPolyRanWithRefinement(poly::UPolynomial&& p,
                                               const Rational& upper);
 
 /**
- * Constructs a CVC4::RealAlgebraicNumber, simply wrapping
+ * Constructs a CVC5::RealAlgebraicNumber, simply wrapping
  * toPolyRanWithRefinement.
  */
 RealAlgebraicNumber toRanWithRefinement(poly::UPolynomial&& p,
@@ -138,7 +138,7 @@ void getVariableInformation(VariableInformation& vi,
                             const poly::Polynomial& poly);
 
 }  // namespace poly_utils
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
 
diff --git a/src/util/random.cpp b/src/util/random.cpp
index 9d94ff624..ab35bd389 100644
--- a/src/util/random.cpp
+++ b/src/util/random.cpp
@@ -21,7 +21,7 @@
 #include <cfloat>
 #include "base/check.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 Random::Random(uint64_t seed) { setSeed(seed); }
 
@@ -66,4 +66,4 @@ bool Random::pickWithProb(double probability)
   return r < p;
 }
 
-}
+}  // namespace CVC5
diff --git a/src/util/random.h b/src/util/random.h
index 31d93a643..67d4e052d 100644
--- a/src/util/random.h
+++ b/src/util/random.h
@@ -21,7 +21,7 @@
 #ifndef CVC4__UTIL__RANDOM_H
 #define CVC4__UTIL__RANDOM_H
 
-namespace CVC4 {
+namespace CVC5 {
 
 class Random
 {
@@ -69,5 +69,5 @@ class Random
   uint64_t d_state;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 #endif
diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index 4d948415f..a974a6155 100644
--- a/src/util/rational_cln_imp.cpp
+++ b/src/util/rational_cln_imp.cpp
@@ -28,7 +28,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 
 /* Computes a rational given a decimal string. The rational
  * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>.
@@ -117,4 +117,4 @@ Maybe<Rational> Rational::fromDouble(double d)
   }
 }
 
-} /* namespace CVC4 */
+} // namespace CVC5
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index bd48ad851..d2c57e90d 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -37,7 +37,7 @@
 #include "util/integer.h"
 #include "util/maybe.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  ** A multi-precision rational constant.
@@ -336,11 +336,11 @@ class CVC4_EXPORT Rational
 
 struct RationalHashFunction
 {
-  inline size_t operator()(const CVC4::Rational& r) const { return r.hash(); }
+  inline size_t operator()(const CVC5::Rational& r) const { return r.hash(); }
 }; /* struct RationalHashFunction */
 
 std::ostream& operator<<(std::ostream& os, const Rational& n) CVC4_EXPORT;
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__RATIONAL_H */
diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp
index 2fbe45d80..0762e17c1 100644
--- a/src/util/rational_gmp_imp.cpp
+++ b/src/util/rational_gmp_imp.cpp
@@ -27,7 +27,7 @@
 
 #include "base/check.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 std::ostream& operator<<(std::ostream& os, const Rational& q){
   return os << q.toString();
@@ -98,4 +98,4 @@ Maybe<Rational> Rational::fromDouble(double d)
   return Maybe<Rational>();
 }
 
-} /* namespace CVC4 */
+} // namespace CVC5
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index 490211001..0d7569b21 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -29,7 +29,7 @@
 #include "util/integer.h"
 #include "util/maybe.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  ** A multi-precision rational constant.
@@ -326,11 +326,11 @@ class CVC4_EXPORT Rational
 
 struct RationalHashFunction
 {
-  inline size_t operator()(const CVC4::Rational& r) const { return r.hash(); }
+  inline size_t operator()(const CVC5::Rational& r) const { return r.hash(); }
 }; /* struct RationalHashFunction */
 
 std::ostream& operator<<(std::ostream& os, const Rational& n) CVC4_EXPORT;
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__RATIONAL_H */
diff --git a/src/util/real_algebraic_number_poly_imp.cpp b/src/util/real_algebraic_number_poly_imp.cpp
index b4730c1b1..6a8111b55 100644
--- a/src/util/real_algebraic_number_poly_imp.cpp
+++ b/src/util/real_algebraic_number_poly_imp.cpp
@@ -28,7 +28,7 @@
 #include "base/check.h"
 #include "util/poly_util.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 RealAlgebraicNumber::RealAlgebraicNumber(poly::AlgebraicNumber&& an)
     : d_value(std::move(an))
@@ -174,4 +174,4 @@ int sgn(const RealAlgebraicNumber& ran) { return sgn(ran.getValue()); }
 bool isZero(const RealAlgebraicNumber& ran) { return is_zero(ran.getValue()); }
 bool isOne(const RealAlgebraicNumber& ran) { return is_one(ran.getValue()); }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/util/real_algebraic_number_poly_imp.h b/src/util/real_algebraic_number_poly_imp.h
index ef5ff16f1..4819e8866 100644
--- a/src/util/real_algebraic_number_poly_imp.h
+++ b/src/util/real_algebraic_number_poly_imp.h
@@ -26,7 +26,7 @@
 #include "util/integer.h"
 #include "util/rational.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * Represents a real algebraic number based on poly::AlgebraicNumber.
@@ -148,6 +148,6 @@ bool isZero(const RealAlgebraicNumber& ran);
 /** Check whether a real algebraic number is one. */
 bool isOne(const RealAlgebraicNumber& ran);
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__REAL_ALGEBRAIC_NUMBER_H */
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index eabafeb37..5df83b1ce 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -16,7 +16,7 @@
 
 #include <ostream>
 
-namespace CVC4 {
+namespace CVC5 {
 
 RegExpRepeat::RegExpRepeat(uint32_t repeatAmount) : d_repeatAmount(repeatAmount)
 {
@@ -57,4 +57,4 @@ std::ostream& operator<<(std::ostream& os, const RegExpLoop& r)
   return os << "[" << r.d_loopMinOcc << ".." << r.d_loopMaxOcc << "]";
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/util/regexp.h b/src/util/regexp.h
index b08065a25..c28f121c0 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -19,7 +19,7 @@
 
 #include <iosfwd>
 
-namespace CVC4 {
+namespace CVC5 {
 
 struct RegExpRepeat
 {
@@ -69,6 +69,6 @@ std::ostream& operator<<(std::ostream& os, const RegExpRepeat& bv);
 
 std::ostream& operator<<(std::ostream& os, const RegExpLoop& bv);
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__UTIL__REGEXP_H */
diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index c31300077..00395178c 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -28,7 +28,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 
 bool WallClockTimer::on() const
 {
@@ -420,4 +420,4 @@ void ResourceManager::registerListener(Listener* listener)
   return d_listeners.push_back(listener);
 }
 
-} /* namespace CVC4 */
+} // namespace CVC5
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index a8a7edb75..3a6269e99 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -26,7 +26,7 @@
 #include <memory>
 #include <vector>
 
-namespace CVC4 {
+namespace CVC5 {
 
 class Listener;
 class Options;
@@ -206,6 +206,6 @@ class ResourceManager
 
 }; /* class ResourceManager */
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__RESOURCE_MANAGER_H */
diff --git a/src/util/result.cpp b/src/util/result.cpp
index 6e83953a3..f9fa94266 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -26,7 +26,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 
 Result::Result()
     : d_sat(SAT_UNKNOWN),
@@ -374,4 +374,4 @@ void Result::toStream(std::ostream& out, OutputLanguage language) const {
   };
 }
 
-} /* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/util/result.h b/src/util/result.h
index b5c5451ea..e2a3a268a 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -24,7 +24,7 @@
 
 #include "options/language.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class Result;
 
@@ -160,6 +160,6 @@ bool operator==(enum Result::Entailment e, const Result& r);
 bool operator!=(enum Result::Sat s, const Result& r);
 bool operator!=(enum Result::Entailment e, const Result& r);
 
-} /* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__RESULT_H */
diff --git a/src/util/roundingmode.h b/src/util/roundingmode.h
index 485bbf847..e58689df6 100644
--- a/src/util/roundingmode.h
+++ b/src/util/roundingmode.h
@@ -18,7 +18,7 @@
 
 #include <fenv.h>
 
-namespace CVC4 {
+namespace CVC5 {
 
 #define CVC4_NUM_ROUNDING_MODES 5
 
@@ -45,6 +45,6 @@ struct RoundingModeHashFunction
   inline size_t operator()(const RoundingMode& rm) const { return size_t(rm); }
 }; /* struct RoundingModeHashFunction */
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/util/safe_print.cpp b/src/util/safe_print.cpp
index adb051d70..c70119822 100644
--- a/src/util/safe_print.cpp
+++ b/src/util/safe_print.cpp
@@ -28,7 +28,7 @@
 /* Size of buffers used */
 #define BUFFER_SIZE 20
 
-namespace CVC4 {
+namespace CVC5 {
 
 template <>
 void safe_print(int fd, const std::string& msg) {
@@ -214,4 +214,4 @@ void safe_print_right_aligned(int fd, uint64_t i, ssize_t width) {
   }
 }
 
-} /* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/util/safe_print.h b/src/util/safe_print.h
index dd66ed41b..553f78bb7 100644
--- a/src/util/safe_print.h
+++ b/src/util/safe_print.h
@@ -44,7 +44,7 @@
 
 #include "cvc4_export.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * Prints arrays of chars (e.g. string literals) of length N. Safe to use in a
@@ -136,6 +136,6 @@ void safe_print_hex(int fd, uint64_t i);
  */
 void safe_print_right_aligned(int fd, uint64_t i, ssize_t width);
 
-} /* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__SAFE_PRINT_H */
diff --git a/src/util/sampler.cpp b/src/util/sampler.cpp
index 05f617aa5..a39aebc63 100644
--- a/src/util/sampler.cpp
+++ b/src/util/sampler.cpp
@@ -23,7 +23,7 @@
 #include "util/bitvector.h"
 #include "util/random.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 BitVector Sampler::pickBvUniform(unsigned sz)
 {
@@ -172,4 +172,4 @@ FloatingPoint Sampler::pickFpBiased(unsigned e, unsigned s)
   return FloatingPoint(e, s, bv);
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/util/sampler.h b/src/util/sampler.h
index 449ef96f9..f715536bc 100644
--- a/src/util/sampler.h
+++ b/src/util/sampler.h
@@ -22,7 +22,7 @@
 
 #include "util/floatingpoint.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class Sampler
 {
@@ -52,6 +52,6 @@ class Sampler
   static constexpr double probSpecial = 0.2;
 };
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__UTIL_FLOATINGPOINT_SAMPLER_H */
diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp
index 91ef8a271..3c93ef5ae 100644
--- a/src/util/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -33,7 +33,7 @@
 #include "util/ostream_util.h"
 #include "util/smt2_quote_string.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 const int PrettySExprs::s_iosIndex = std::ios_base::xalloc();
 
@@ -90,12 +90,14 @@ SExpr::SExpr(const SExpr& other)
   Assert((d_children == NULL) == isAtom());
 }
 
-SExpr::SExpr(const CVC4::Integer& value)
+SExpr::SExpr(const CVC5::Integer& value)
     : d_sexprType(SEXPR_INTEGER),
       d_integerValue(value),
       d_rationalValue(0),
       d_stringValue(""),
-      d_children(NULL) {}
+      d_children(NULL)
+{
+}
 
 SExpr::SExpr(int value)
     : d_sexprType(SEXPR_INTEGER),
@@ -125,12 +127,14 @@ SExpr::SExpr(unsigned long int value)
       d_stringValue(""),
       d_children(NULL) {}
 
-SExpr::SExpr(const CVC4::Rational& value)
+SExpr::SExpr(const CVC5::Rational& value)
     : d_sexprType(SEXPR_RATIONAL),
       d_integerValue(0),
       d_rationalValue(value),
       d_stringValue(""),
-      d_children(NULL) {}
+      d_children(NULL)
+{
+}
 
 SExpr::SExpr(const std::string& value)
     : d_sexprType(SEXPR_STRING),
@@ -304,12 +308,14 @@ std::string SExpr::getValue() const {
   return std::string();
 }
 
-const CVC4::Integer& SExpr::getIntegerValue() const {
+const CVC5::Integer& SExpr::getIntegerValue() const
+{
   PrettyCheckArgument(isInteger(), this);
   return d_integerValue;
 }
 
-const CVC4::Rational& SExpr::getRationalValue() const {
+const CVC5::Rational& SExpr::getRationalValue() const
+{
   PrettyCheckArgument(isRational(), this);
   return d_rationalValue;
 }
@@ -377,4 +383,4 @@ SExpr SExpr::parseListOfListOfAtoms(
   return SExpr(parsedListsOfAtoms);
 }
 
-} /* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index aabbf473d..f4eaca663 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -35,7 +35,7 @@
 #include "util/integer.h"
 #include "util/rational.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class SExprKeyword
 {
@@ -61,14 +61,14 @@ class CVC4_EXPORT SExpr
   SExpr& operator=(const SExpr& other);
   ~SExpr();
 
-  SExpr(const CVC4::Integer& value);
+  SExpr(const CVC5::Integer& value);
 
   SExpr(int value);
   SExpr(long int value);
   SExpr(unsigned int value);
   SExpr(unsigned long int value);
 
-  SExpr(const CVC4::Rational& value);
+  SExpr(const CVC5::Rational& value);
 
   SExpr(const std::string& value);
 
@@ -120,13 +120,13 @@ class CVC4_EXPORT SExpr
    * Get the integer value of this S-expression. This will cause an
    * error if this S-expression is not an integer.
    */
-  const CVC4::Integer& getIntegerValue() const;
+  const CVC5::Integer& getIntegerValue() const;
 
   /**
    * Get the rational value of this S-expression. This will cause an
    * error if this S-expression is not a rational.
    */
-  const CVC4::Rational& getRationalValue() const;
+  const CVC5::Rational& getRationalValue() const;
 
   /**
    * Get the children of this S-expression. This will cause an error
@@ -211,10 +211,10 @@ class CVC4_EXPORT SExpr
   } d_sexprType;
 
   /** The value of an atomic integer-valued S-expression. */
-  CVC4::Integer d_integerValue;
+  CVC5::Integer d_integerValue;
 
   /** The value of an atomic rational-valued S-expression. */
-  CVC4::Rational d_rationalValue;
+  CVC5::Rational d_rationalValue;
 
   /** The value of an atomic S-expression. */
   std::string d_stringValue;
@@ -301,6 +301,6 @@ class CVC4_EXPORT PrettySExprs
  */
 std::ostream& operator<<(std::ostream& out, PrettySExprs ps);
 
-} /* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__SEXPR_H */
diff --git a/src/util/smt2_quote_string.cpp b/src/util/smt2_quote_string.cpp
index e06e5dc93..7d255c6f1 100644
--- a/src/util/smt2_quote_string.cpp
+++ b/src/util/smt2_quote_string.cpp
@@ -19,7 +19,7 @@
 #include <sstream>
 #include <string>
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * SMT-LIB 2 quoting for symbols
@@ -43,4 +43,4 @@ std::string quoteSymbol(const std::string& s){
   return s;
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/util/smt2_quote_string.h b/src/util/smt2_quote_string.h
index 911faae42..b9e6592df 100644
--- a/src/util/smt2_quote_string.h
+++ b/src/util/smt2_quote_string.h
@@ -21,13 +21,13 @@
 
 #include <string>
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * SMT-LIB 2 quoting for symbols
  */
 std::string quoteSymbol(const std::string& s);
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__UTIL__SMT2_QUOTE_STRING_H */
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
index d824e0f21..3c7ac6731 100644
--- a/src/util/statistics.cpp
+++ b/src/util/statistics.cpp
@@ -20,8 +20,7 @@
 #include "util/safe_print.h"
 #include "util/statistics_registry.h" // for details about class Stat
 
-
-namespace CVC4 {
+namespace CVC5 {
 
 bool StatisticsBase::StatCmp::operator()(const Stat* s1, const Stat* s2) const {
   return s1->getName() < s2->getName();
@@ -131,4 +130,4 @@ SExpr StatisticsBase::getStatistic(std::string name) const {
   }
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/util/statistics.h b/src/util/statistics.h
index 7b5400aaf..0c52cfe8e 100644
--- a/src/util/statistics.h
+++ b/src/util/statistics.h
@@ -29,7 +29,7 @@
 #include "cvc4_export.h"
 #include "util/sexpr.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class Stat;
 
@@ -127,6 +127,6 @@ public:
 
 }; /* class Statistics */
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__STATISTICS_H */
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index b439daba8..bbd98ffaf 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -34,7 +34,7 @@
 /****************************************************************************/
 /* Some utility functions for timespec                                    */
 /****************************************************************************/
-namespace CVC4 {
+namespace CVC5 {
 
 void StatisticsRegistry::registerStat(Stat* s)
 {
@@ -89,4 +89,4 @@ RegisterStatistic::~RegisterStatistic() {
   d_reg->unregisterStat(d_stat);
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index a55aec282..b8c83436f 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -102,7 +102,7 @@
 #include "util/statistics.h"
 #include "util/stats_base.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /** A statistic that contains a SExpr. */
 class SExprStat : public Stat {
@@ -196,6 +196,6 @@ private:
 
 }; /* class RegisterStatistic */
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__STATISTICS_REGISTRY_H */
diff --git a/src/util/stats_base.cpp b/src/util/stats_base.cpp
index f55e2f5ab..758883cbe 100644
--- a/src/util/stats_base.cpp
+++ b/src/util/stats_base.cpp
@@ -18,7 +18,7 @@
 
 #include "util/statistics_registry.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 Stat::Stat(const std::string& name) : d_name(name)
 {
@@ -112,4 +112,4 @@ SExpr AverageStat::getValue() const
   return SExpr(Rational::fromDecimal(ss.str()));
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/util/stats_base.h b/src/util/stats_base.h
index 24a2ca560..f7d19624a 100644
--- a/src/util/stats_base.h
+++ b/src/util/stats_base.h
@@ -34,7 +34,7 @@
 #define CVC4_USE_STATISTICS false
 #endif
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * The base class for all statistics.
@@ -274,6 +274,6 @@ class SizeStat : public Stat
   const T& d_sized;
 }; /* class SizeStat */
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/util/stats_histogram.h b/src/util/stats_histogram.h
index 49306ba28..44d4b9e7c 100644
--- a/src/util/stats_histogram.h
+++ b/src/util/stats_histogram.h
@@ -24,7 +24,7 @@
 
 #include "util/stats_base.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /**
  * A histogram statistic class for integral types.
@@ -123,6 +123,6 @@ class IntegralHistogramStat : public Stat
   int64_t d_offset;
 }; /* class IntegralHistogramStat */
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/util/stats_timer.cpp b/src/util/stats_timer.cpp
index 63d9914d6..6280b79e1 100644
--- a/src/util/stats_timer.cpp
+++ b/src/util/stats_timer.cpp
@@ -21,7 +21,7 @@
 #include "base/check.h"
 #include "util/ostream_util.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 template <>
 void safe_print(int fd, const timer_stat_detail::duration& t)
@@ -101,4 +101,4 @@ CodeTimer::~CodeTimer()
   }
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/util/stats_timer.h b/src/util/stats_timer.h
index 36e254795..40df52ade 100644
--- a/src/util/stats_timer.h
+++ b/src/util/stats_timer.h
@@ -24,7 +24,7 @@
 #include "cvc4_export.h"
 #include "util/stats_base.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace timer_stat_detail {
 using clock = std::chrono::steady_clock;
 using time_point = clock::time_point;
@@ -46,7 +46,7 @@ class CodeTimer;
 class CVC4_EXPORT TimerStat : public BackedStat<timer_stat_detail::duration>
 {
  public:
-  typedef CVC4::CodeTimer CodeTimer;
+  typedef CVC5::CodeTimer CodeTimer;
 
   /**
    * Construct a timer statistic with the given name.  Newly-constructed
@@ -108,6 +108,6 @@ private:
   CodeTimer& operator=(const CodeTimer& timer) = delete;
 }; /* class CodeTimer */
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/util/stats_utils.cpp b/src/util/stats_utils.cpp
index 893afcb4c..2a87ff439 100644
--- a/src/util/stats_utils.cpp
+++ b/src/util/stats_utils.cpp
@@ -23,7 +23,7 @@
 #include "util/ostream_util.h"
 #include "util/stats_timer.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 std::ostream& operator<<(std::ostream& os,
                          const timer_stat_detail::duration& dur)
@@ -35,4 +35,4 @@ std::ostream& operator<<(std::ostream& os,
             << (dur % std::chrono::seconds(1)).count();
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/util/stats_utils.h b/src/util/stats_utils.h
index b38f7b641..d511539ca 100644
--- a/src/util/stats_utils.h
+++ b/src/util/stats_utils.h
@@ -23,7 +23,7 @@
 
 #include "cvc4_export.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 namespace timer_stat_detail {
 struct duration;
@@ -32,6 +32,6 @@ struct duration;
 std::ostream& operator<<(std::ostream& os,
                          const timer_stat_detail::duration& dur) CVC4_EXPORT;
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/util/string.cpp b/src/util/string.cpp
index 73a0d78ee..d1d7fadc2 100644
--- a/src/util/string.cpp
+++ b/src/util/string.cpp
@@ -25,7 +25,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 
 static_assert(UCHAR_MAX == 255, "Unsigned char is assumed to have 256 values.");
 
@@ -101,7 +101,7 @@ void String::addCharToInternal(unsigned char ch, std::vector<unsigned>& str)
     std::stringstream serr;
     serr << "Illegal string character: \"" << ch
          << "\", must use escape sequence";
-    throw CVC4::Exception(serr.str());
+    throw CVC5::Exception(serr.str());
   }
   else
   {
@@ -513,4 +513,4 @@ std::ostream &operator<<(std::ostream &os, const String &s) {
   return os << "\"" << s.toString() << "\"";
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/util/string.h b/src/util/string.h
index 6c620587a..a3e0245aa 100644
--- a/src/util/string.h
+++ b/src/util/string.h
@@ -23,7 +23,7 @@
 
 #include "util/rational.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 /** The CVC4 string class
  *
@@ -46,7 +46,7 @@ class String
   static inline unsigned num_codes() { return 196608; }
   /** constructors for String
    *
-   * Internally, a CVC4::String is represented by a vector of unsigned
+   * Internally, a CVC5::String is represented by a vector of unsigned
    * integers (d_str) representing the code points of the characters.
    *
    * To build a string from a C++ string, we may process escape sequences
@@ -61,7 +61,7 @@ class String
    * where d_0 ... d_4 are hexadecimal digits, to the appropriate character.
    *
    * If useEscSequences is false, then the characters of the constructed
-   * CVC4::String correspond one-to-one with the input string.
+   * CVC5::String correspond one-to-one with the input string.
    */
   String() = default;
   explicit String(const std::string& s, bool useEscSequences = false)
@@ -112,7 +112,7 @@ class String
    * If useEscSequences is false, the string's printable characters are
    * printed as characters. Notice that for all std::string s having only
    * printable characters, we have that
-   *    CVC4::String( s ).toString() = s.
+   *    CVC5::String( s ).toString() = s.
    */
   std::string toString(bool useEscSequences = false) const;
   /* toWString
@@ -265,7 +265,8 @@ namespace strings {
 
 struct StringHashFunction
 {
-  size_t operator()(const ::CVC4::String& s) const {
+  size_t operator()(const ::CVC5::String& s) const
+  {
     return std::hash<std::string>()(s.toString());
   }
 }; /* struct StringHashFunction */
@@ -274,6 +275,6 @@ struct StringHashFunction
 
 std::ostream& operator<<(std::ostream& os, const String& s);
 
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__UTIL__STRING_H */
diff --git a/src/util/tuple.h b/src/util/tuple.h
index d77d7bf97..571bfe797 100644
--- a/src/util/tuple.h
+++ b/src/util/tuple.h
@@ -23,7 +23,7 @@
 #include <vector>
 #include <utility>
 
-namespace CVC4 {
+namespace CVC5 {
 
 class TupleUpdate
 {
@@ -49,6 +49,6 @@ inline std::ostream& operator<<(std::ostream& out, const TupleUpdate& t) {
   return out << "[" << t.getIndex() << "]";
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__TUPLE_H */
diff --git a/src/util/unsafe_interrupt_exception.h b/src/util/unsafe_interrupt_exception.h
index 29c22409c..31fe26577 100644
--- a/src/util/unsafe_interrupt_exception.h
+++ b/src/util/unsafe_interrupt_exception.h
@@ -21,9 +21,9 @@
 #include "base/exception.h"
 #include "cvc4_export.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
-class CVC4_EXPORT UnsafeInterruptException : public CVC4::Exception
+class CVC4_EXPORT UnsafeInterruptException : public CVC5::Exception
 {
  public:
   UnsafeInterruptException() :
@@ -40,6 +40,6 @@ class CVC4_EXPORT UnsafeInterruptException : public CVC4::Exception
   }
 }; /* class UnsafeInterruptException */
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__UNSAFE_INTERRUPT_EXCEPTION_H */
diff --git a/src/util/utility.cpp b/src/util/utility.cpp
index 6ce331fc4..480b68ff2 100644
--- a/src/util/utility.cpp
+++ b/src/util/utility.cpp
@@ -22,7 +22,7 @@
 
 #include "base/check.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 std::unique_ptr<std::fstream> openTmpFile(std::string* pattern)
 {
@@ -52,4 +52,4 @@ std::unique_ptr<std::fstream> openTmpFile(std::string* pattern)
   return tmpStream;
 }
 
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/util/utility.h b/src/util/utility.h
index 411d3a6f3..006f2072c 100644
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -24,8 +24,7 @@
 #include <memory>
 #include <string>
 
-namespace CVC4 {
-
+namespace CVC5 {
 
 /**
  * Using std::find_if(), finds the first iterator in [first,last)
@@ -78,6 +77,6 @@ void container_to_stream(std::ostream& out,
  */
 std::unique_ptr<std::fstream> openTmpFile(std::string* pattern);
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__UTILITY_H */