Rename namespace CVC5 to cvc5. (#6258)

29 files changed, 93 insertions, 93 deletions

diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp
index fd80a03f7..478ce58cd 100644
--- a/src/theory/bags/bag_solver.cpp
+++ b/src/theory/bags/bag_solver.cpp
@@ -24,10 +24,10 @@
 #include "theory/uf/equality_engine_iterator.h"
 
 using namespace std;
-using namespace CVC5::context;
-using namespace CVC5::kind;
+using namespace cvc5::context;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -212,4 +212,4 @@ void BagSolver::checkDisequalBagTerms()
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bags/bag_solver.h b/src/theory/bags/bag_solver.h
index 9d0e597dd..5cd7ed338 100644
--- a/src/theory/bags/bag_solver.h
+++ b/src/theory/bags/bag_solver.h
@@ -19,7 +19,7 @@
 
 #include "theory/bags/inference_generator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -90,6 +90,6 @@ class BagSolver
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BAG__SOLVER_H */
diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp
index ccee08aab..f4670f8be 100644
--- a/src/theory/bags/bags_rewriter.cpp
+++ b/src/theory/bags/bags_rewriter.cpp
@@ -16,9 +16,9 @@
 
 #include "theory/bags/normal_form.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -503,4 +503,4 @@ BagsRewriteResponse BagsRewriter::postRewriteEqual(const TNode& n) const
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h
index 4552ed9da..bc66d7efa 100644
--- a/src/theory/bags/bags_rewriter.h
+++ b/src/theory/bags/bags_rewriter.h
@@ -22,7 +22,7 @@
 #include "util/statistics_registry.h"
 #include "util/stats_histogram.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -223,6 +223,6 @@ class BagsRewriter : public TheoryRewriter
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BAGS__THEORY_BAGS_REWRITER_H */
diff --git a/src/theory/bags/bags_statistics.cpp b/src/theory/bags/bags_statistics.cpp
index 369831c70..6c88ffb43 100644
--- a/src/theory/bags/bags_statistics.cpp
+++ b/src/theory/bags/bags_statistics.cpp
@@ -16,7 +16,7 @@
 
 #include "smt/smt_statistics_registry.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -32,4 +32,4 @@ BagsStatistics::~BagsStatistics()
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bags/bags_statistics.h b/src/theory/bags/bags_statistics.h
index e0a1c4133..ac60fbc3e 100644
--- a/src/theory/bags/bags_statistics.h
+++ b/src/theory/bags/bags_statistics.h
@@ -21,7 +21,7 @@
 #include "util/statistics_registry.h"
 #include "util/stats_histogram.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -40,6 +40,6 @@ class BagsStatistics
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BAGS_STATISTICS_H */
diff --git a/src/theory/bags/infer_info.cpp b/src/theory/bags/infer_info.cpp
index 444597eb5..c0fac0753 100644
--- a/src/theory/bags/infer_info.cpp
+++ b/src/theory/bags/infer_info.cpp
@@ -16,7 +16,7 @@
 
 #include "theory/bags/inference_manager.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -79,4 +79,4 @@ std::ostream& operator<<(std::ostream& out, const InferInfo& ii)
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bags/infer_info.h b/src/theory/bags/infer_info.h
index 18765bbe7..508c49fe5 100644
--- a/src/theory/bags/infer_info.h
+++ b/src/theory/bags/infer_info.h
@@ -24,7 +24,7 @@
 #include "theory/inference_id.h"
 #include "theory/theory_inference.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 class TheoryInferenceManager;
@@ -85,6 +85,6 @@ std::ostream& operator<<(std::ostream& out, const InferInfo& ii);
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BAGS__INFER_INFO_H */
diff --git a/src/theory/bags/inference_generator.cpp b/src/theory/bags/inference_generator.cpp
index 2f6a36b9c..57a306820 100644
--- a/src/theory/bags/inference_generator.cpp
+++ b/src/theory/bags/inference_generator.cpp
@@ -21,7 +21,7 @@
 #include "theory/bags/solver_state.h"
 #include "theory/uf/equality_engine.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -270,4 +270,4 @@ Node InferenceGenerator::getMultiplicityTerm(Node element, Node bag)
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bags/inference_generator.h b/src/theory/bags/inference_generator.h
index 4f0b498c2..baa391f38 100644
--- a/src/theory/bags/inference_generator.h
+++ b/src/theory/bags/inference_generator.h
@@ -20,7 +20,7 @@
 #include "expr/node.h"
 #include "infer_info.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -188,6 +188,6 @@ class InferenceGenerator
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BAGS__INFERENCE_GENERATOR_H */
diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp
index 3fa425f7a..422fb53d0 100644
--- a/src/theory/bags/inference_manager.cpp
+++ b/src/theory/bags/inference_manager.cpp
@@ -17,9 +17,9 @@
 #include "theory/bags/solver_state.h"
 
 using namespace std;
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -48,4 +48,4 @@ void InferenceManager::doPending()
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h
index 34f6621aa..68d923889 100644
--- a/src/theory/bags/inference_manager.h
+++ b/src/theory/bags/inference_manager.h
@@ -19,7 +19,7 @@
 
 #include "theory/inference_manager_buffered.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -63,6 +63,6 @@ class InferenceManager : public InferenceManagerBuffered
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BAGS__INFERENCE_MANAGER_H */
diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds
index dd8eacfb5..038e7dd7f 100644
--- a/src/theory/bags/kinds
+++ b/src/theory/bags/kinds
@@ -5,10 +5,10 @@
 #
 
 theory THEORY_BAGS \
-    ::CVC5::theory::bags::TheoryBags \
+    ::cvc5::theory::bags::TheoryBags \
     "theory/bags/theory_bags.h"
 typechecker "theory/bags/theory_bags_type_rules.h"
-rewriter ::CVC5::theory::bags::BagsRewriter \
+rewriter ::cvc5::theory::bags::BagsRewriter \
     "theory/bags/bags_rewriter.h"
 
 properties parametric
@@ -16,22 +16,22 @@ properties check presolve
 
 # constants
 constant EMPTYBAG \
-    ::CVC5::EmptyBag \
-    ::CVC5::EmptyBagHashFunction \
+    ::cvc5::EmptyBag \
+    ::cvc5::EmptyBagHashFunction \
     "expr/emptybag.h" \
-    "the empty bag constant; payload is an instance of the CVC5::EmptyBag class"
+    "the empty bag constant; payload is an instance of the cvc5::EmptyBag class"
 
 # the type
 operator BAG_TYPE 1 "bag type, takes as parameter the type of the elements"
 cardinality BAG_TYPE \
-    "::CVC5::theory::bags::BagsProperties::computeCardinality(%TYPE%)" \
+    "::cvc5::theory::bags::BagsProperties::computeCardinality(%TYPE%)" \
     "theory/bags/theory_bags_type_rules.h"
 well-founded BAG_TYPE \
-    "::CVC5::theory::bags::BagsProperties::isWellFounded(%TYPE%)" \
-    "::CVC5::theory::bags::BagsProperties::mkGroundTerm(%TYPE%)" \
+    "::cvc5::theory::bags::BagsProperties::isWellFounded(%TYPE%)" \
+    "::cvc5::theory::bags::BagsProperties::mkGroundTerm(%TYPE%)" \
     "theory/bags/theory_bags_type_rules.h"
 enumerator BAG_TYPE \
-    "::CVC5::theory::bags::BagEnumerator" \
+    "::cvc5::theory::bags::BagEnumerator" \
     "theory/bags/theory_bags_type_enumerator.h"
 
 # operators
@@ -50,10 +50,10 @@ operator BAG_COUNT         2  "multiplicity of an element in a bag"
 operator DUPLICATE_REMOVAL 1  "eliminate duplicates in a bag (also known as the delta operator,or the squash operator)"
 
 constant MK_BAG_OP \
-	::CVC5::MakeBagOp \
-	::CVC5::MakeBagOpHashFunction \
+	::cvc5::MakeBagOp \
+	::cvc5::MakeBagOpHashFunction \
 	"theory/bags/make_bag_op.h" \
-	"operator for MK_BAG; payload is an instance of the CVC5::MakeBagOp class"
+	"operator for MK_BAG; payload is an instance of the cvc5::MakeBagOp class"
 parameterized MK_BAG MK_BAG_OP 2 \
 "constructs a bag from one element along with its multiplicity"
 
@@ -70,24 +70,24 @@ operator BAG_TO_SET        1  "converts a bag to a set"
 # If the bag has cardinality > 1, then (choose A) will deterministically return an element in A.
 operator BAG_CHOOSE        1  "return an element in the bag given as a parameter"
 
-typerule UNION_MAX           ::CVC5::theory::bags::BinaryOperatorTypeRule
-typerule UNION_DISJOINT      ::CVC5::theory::bags::BinaryOperatorTypeRule
-typerule INTERSECTION_MIN    ::CVC5::theory::bags::BinaryOperatorTypeRule
-typerule DIFFERENCE_SUBTRACT ::CVC5::theory::bags::BinaryOperatorTypeRule
-typerule DIFFERENCE_REMOVE   ::CVC5::theory::bags::BinaryOperatorTypeRule
-typerule SUBBAG              ::CVC5::theory::bags::SubBagTypeRule
-typerule BAG_COUNT           ::CVC5::theory::bags::CountTypeRule
-typerule DUPLICATE_REMOVAL   ::CVC5::theory::bags::DuplicateRemovalTypeRule
+typerule UNION_MAX           ::cvc5::theory::bags::BinaryOperatorTypeRule
+typerule UNION_DISJOINT      ::cvc5::theory::bags::BinaryOperatorTypeRule
+typerule INTERSECTION_MIN    ::cvc5::theory::bags::BinaryOperatorTypeRule
+typerule DIFFERENCE_SUBTRACT ::cvc5::theory::bags::BinaryOperatorTypeRule
+typerule DIFFERENCE_REMOVE   ::cvc5::theory::bags::BinaryOperatorTypeRule
+typerule SUBBAG              ::cvc5::theory::bags::SubBagTypeRule
+typerule BAG_COUNT           ::cvc5::theory::bags::CountTypeRule
+typerule DUPLICATE_REMOVAL   ::cvc5::theory::bags::DuplicateRemovalTypeRule
 typerule MK_BAG_OP           "SimpleTypeRule<RBuiltinOperator>"
-typerule MK_BAG              ::CVC5::theory::bags::MkBagTypeRule
-typerule EMPTYBAG            ::CVC5::theory::bags::EmptyBagTypeRule
-typerule BAG_CARD            ::CVC5::theory::bags::CardTypeRule
-typerule BAG_CHOOSE          ::CVC5::theory::bags::ChooseTypeRule
-typerule BAG_IS_SINGLETON    ::CVC5::theory::bags::IsSingletonTypeRule
-typerule BAG_FROM_SET        ::CVC5::theory::bags::FromSetTypeRule
-typerule BAG_TO_SET          ::CVC5::theory::bags::ToSetTypeRule
+typerule MK_BAG              ::cvc5::theory::bags::MkBagTypeRule
+typerule EMPTYBAG            ::cvc5::theory::bags::EmptyBagTypeRule
+typerule BAG_CARD            ::cvc5::theory::bags::CardTypeRule
+typerule BAG_CHOOSE          ::cvc5::theory::bags::ChooseTypeRule
+typerule BAG_IS_SINGLETON    ::cvc5::theory::bags::IsSingletonTypeRule
+typerule BAG_FROM_SET        ::cvc5::theory::bags::FromSetTypeRule
+typerule BAG_TO_SET          ::cvc5::theory::bags::ToSetTypeRule
 
-construle UNION_DISJOINT     ::CVC5::theory::bags::BinaryOperatorTypeRule
-construle MK_BAG             ::CVC5::theory::bags::MkBagTypeRule
+construle UNION_DISJOINT     ::cvc5::theory::bags::BinaryOperatorTypeRule
+construle MK_BAG             ::cvc5::theory::bags::MkBagTypeRule
 
 endtheory
diff --git a/src/theory/bags/make_bag_op.cpp b/src/theory/bags/make_bag_op.cpp
index 15e3a30c7..168379390 100644
--- a/src/theory/bags/make_bag_op.cpp
+++ b/src/theory/bags/make_bag_op.cpp
@@ -18,7 +18,7 @@
 
 #include "expr/type_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 std::ostream& operator<<(std::ostream& out, const MakeBagOp& op)
 {
@@ -46,4 +46,4 @@ bool MakeBagOp::operator==(const MakeBagOp& op) const
   return getType() == op.getType();
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bags/make_bag_op.h b/src/theory/bags/make_bag_op.h
index 4c2a3e933..44b105225 100644
--- a/src/theory/bags/make_bag_op.h
+++ b/src/theory/bags/make_bag_op.h
@@ -19,7 +19,7 @@
 
 #include <memory>
 
-namespace CVC5 {
+namespace cvc5 {
 
 class TypeNode;
 
@@ -57,6 +57,6 @@ struct MakeBagOpHashFunction
   size_t operator()(const MakeBagOp& op) const;
 }; /* struct MakeBagOpHashFunction */
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__MAKE_BAG_OP_H */
diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp
index 5952b66d8..1773346f0 100644
--- a/src/theory/bags/normal_form.cpp
+++ b/src/theory/bags/normal_form.cpp
@@ -16,9 +16,9 @@
 #include "theory/sets/normal_form.h"
 #include "theory/type_enumerator.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -674,4 +674,4 @@ Node NormalForm::evaluateToSet(TNode n)
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bags/normal_form.h b/src/theory/bags/normal_form.h
index 1c7f05d8e..5b5591133 100644
--- a/src/theory/bags/normal_form.h
+++ b/src/theory/bags/normal_form.h
@@ -19,7 +19,7 @@
 #ifndef CVC4__THEORY__BAGS__NORMAL_FORM_H
 #define CVC4__THEORY__BAGS__NORMAL_FORM_H
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -192,6 +192,6 @@ class NormalForm
 };
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BAGS__NORMAL_FORM_H */
diff --git a/src/theory/bags/rewrites.cpp b/src/theory/bags/rewrites.cpp
index d0299d52a..4d6929346 100644
--- a/src/theory/bags/rewrites.cpp
+++ b/src/theory/bags/rewrites.cpp
@@ -16,7 +16,7 @@
 
 #include <iostream>
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -79,4 +79,4 @@ std::ostream& operator<<(std::ostream& out, Rewrite r)
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bags/rewrites.h b/src/theory/bags/rewrites.h
index 9e7bb54fa..aa49c71fb 100644
--- a/src/theory/bags/rewrites.h
+++ b/src/theory/bags/rewrites.h
@@ -19,7 +19,7 @@
 
 #include <iosfwd>
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -92,6 +92,6 @@ std::ostream& operator<<(std::ostream& out, Rewrite r);
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BAGS__REWRITES_H */
diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp
index 4011a3fc4..aa714a61b 100644
--- a/src/theory/bags/solver_state.cpp
+++ b/src/theory/bags/solver_state.cpp
@@ -20,9 +20,9 @@
 #include "theory/uf/equality_engine.h"
 
 using namespace std;
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -136,4 +136,4 @@ void SolverState::collectDisequalBagTerms()
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h
index e6b2a2504..e7c09db8f 100644
--- a/src/theory/bags/solver_state.h
+++ b/src/theory/bags/solver_state.h
@@ -21,7 +21,7 @@
 
 #include "theory/theory_state.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -90,6 +90,6 @@ class SolverState : public TheoryState
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BAGS__THEORY_SOLVER_STATE_H */
diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp
index 072655834..dd3820c82 100644
--- a/src/theory/bags/term_registry.cpp
+++ b/src/theory/bags/term_registry.cpp
@@ -18,9 +18,9 @@
 #include "theory/bags/solver_state.h"
 
 using namespace std;
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -45,4 +45,4 @@ Node TermRegistry::getEmptyBag(TypeNode tn)
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h
index adf97fd5f..ab519b100 100644
--- a/src/theory/bags/term_registry.h
+++ b/src/theory/bags/term_registry.h
@@ -22,7 +22,7 @@
 #include "context/cdhashmap.h"
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -59,6 +59,6 @@ class TermRegistry
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BAGS__TERM_REGISTRY_H */
diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index f91fd40f0..bea83ce40 100644
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -19,9 +19,9 @@
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -262,4 +262,4 @@ void TheoryBags::NotifyClass::eqNotifyDisequal(TNode n1, TNode n2, TNode reason)
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h
index 6bd9ddc65..7bb6111bd 100644
--- a/src/theory/bags/theory_bags.h
+++ b/src/theory/bags/theory_bags.h
@@ -27,7 +27,7 @@
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -114,6 +114,6 @@ class TheoryBags : public Theory
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BAGS__THEORY_BAGS_H */
diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp
index 02494727c..f34d304fb 100644
--- a/src/theory/bags/theory_bags_type_enumerator.cpp
+++ b/src/theory/bags/theory_bags_type_enumerator.cpp
@@ -18,7 +18,7 @@
 #include "theory/rewriter.h"
 #include "theory_bags_type_enumerator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -83,4 +83,4 @@ bool BagEnumerator::isFinished()
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
\ No newline at end of file
+}  // namespace cvc5
\ No newline at end of file
diff --git a/src/theory/bags/theory_bags_type_enumerator.h b/src/theory/bags/theory_bags_type_enumerator.h
index c13946388..bdf57213d 100644
--- a/src/theory/bags/theory_bags_type_enumerator.h
+++ b/src/theory/bags/theory_bags_type_enumerator.h
@@ -20,7 +20,7 @@
 #include "expr/type_node.h"
 #include "theory/type_enumerator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -86,6 +86,6 @@ class BagEnumerator : public TypeEnumeratorBase<BagEnumerator>
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BAGS__TYPE_ENUMERATOR_H */
\ No newline at end of file
diff --git a/src/theory/bags/theory_bags_type_rules.cpp b/src/theory/bags/theory_bags_type_rules.cpp
index 2acbb1e27..f198d68e9 100644
--- a/src/theory/bags/theory_bags_type_rules.cpp
+++ b/src/theory/bags/theory_bags_type_rules.cpp
@@ -19,7 +19,7 @@
 #include "base/check.h"
 #include "theory/bags/normal_form.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bags {
 
@@ -279,4 +279,4 @@ TypeNode ToSetTypeRule::computeType(NodeManager* nodeManager,
 }
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h
index dd93186ad..f48001c5e 100644
--- a/src/theory/bags/theory_bags_type_rules.h
+++ b/src/theory/bags/theory_bags_type_rules.h
@@ -20,7 +20,7 @@
 #include "expr/node.h"
 #include "expr/type_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 class NodeManager;
 
@@ -102,6 +102,6 @@ struct BagsProperties
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BAGS__THEORY_BAGS_TYPE_RULES_H */