Rename namespace CVC5 to cvc5. (#6258)

author: Aina Niemetz <aina.niemetz@gmail.com> 2021-04-01 09:56:14 -0700
committer: GitHub <noreply@github.com> 2021-04-01 16:56:14 +0000
commit: 05a53a2ac405bcd18a84024247145f161809c3b0 (patch)
tree: 34241c0a82f79d717ddbfbb0c294f9a09c7edb0c /src/theory/quantifiers
parent: afaf4413775ff7d6054a5893f1397ad908e0773c (diff)
236 files changed, 607 insertions, 607 deletions
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index eb977960b..3832508dd 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -15,9 +15,9 @@
 
 #include "theory/quantifiers/alpha_equivalence.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -110,4 +110,4 @@ Node AlphaEquivalence::reduceQuantifier(Node q)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h
index 822b674e2..03047c93b 100644
--- a/src/theory/quantifiers/alpha_equivalence.h
+++ b/src/theory/quantifiers/alpha_equivalence.h
@@ -21,7 +21,7 @@
 
 #include "expr/term_canonize.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -101,6 +101,6 @@ class AlphaEquivalence
 
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index c4bd2c083..014e46925 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -22,9 +22,9 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -442,4 +442,4 @@ Node BvInverter::solveBvLit(Node sv,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h
index c033b26d7..a187cd36a 100644
--- a/src/theory/quantifiers/bv_inverter.h
+++ b/src/theory/quantifiers/bv_inverter.h
@@ -24,7 +24,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -128,6 +128,6 @@ class BvInverter
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__BV_INVERTER_H */
diff --git a/src/theory/quantifiers/bv_inverter_utils.cpp b/src/theory/quantifiers/bv_inverter_utils.cpp
index 459c3f93f..e53e64a94 100644
--- a/src/theory/quantifiers/bv_inverter_utils.cpp
+++ b/src/theory/quantifiers/bv_inverter_utils.cpp
@@ -15,9 +15,9 @@
 #include "theory/quantifiers/bv_inverter_utils.h"
 #include "theory/bv/theory_bv_utils.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace utils {
@@ -2589,4 +2589,4 @@ Node getICBvSext(bool pol, Kind litk, unsigned idx, Node x, Node sv_t, Node t)
 }  // namespace utils
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/bv_inverter_utils.h b/src/theory/quantifiers/bv_inverter_utils.h
index c6400bd60..823855d1b 100644
--- a/src/theory/quantifiers/bv_inverter_utils.h
+++ b/src/theory/quantifiers/bv_inverter_utils.h
@@ -19,7 +19,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace utils {
@@ -68,5 +68,5 @@ Node getICBvSext(bool pol, Kind litk, unsigned idx, Node x, Node sv_t, Node t);
 }  // namespace utils
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 #endif
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 1319e5c38..526469ef2 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -24,10 +24,10 @@
 #include "theory/rewriter.h"
 
 using namespace std;
-using namespace CVC5::kind;
-using namespace CVC5::context;
+using namespace cvc5::kind;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -296,4 +296,4 @@ void CandidateRewriteDatabase::setExtendedRewriter(ExtendedRewriter* er)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h
index 396ef0d03..45333bc76 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.h
+++ b/src/theory/quantifiers/candidate_rewrite_database.h
@@ -23,7 +23,7 @@
 #include "theory/quantifiers/expr_miner.h"
 #include "theory/quantifiers/sygus_sampler.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -128,6 +128,6 @@ class CandidateRewriteDatabase : public ExprMiner
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */
diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp
index 0ab85ccf7..7ada36dc2 100644
--- a/src/theory/quantifiers/candidate_rewrite_filter.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp
@@ -20,9 +20,9 @@
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -277,4 +277,4 @@ bool CandidateRewriteFilter::notify(Node s,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h
index faf675bcb..aa31c7845 100644
--- a/src/theory/quantifiers/candidate_rewrite_filter.h
+++ b/src/theory/quantifiers/candidate_rewrite_filter.h
@@ -25,7 +25,7 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/sygus_sampler.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -171,6 +171,6 @@ class CandidateRewriteFilter
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index 29881a3a4..2a7a95b65 100644
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -25,10 +25,10 @@
 #include "util/random.h"
 
 using namespace std;
-using namespace CVC5::kind;
-using namespace CVC5::context;
+using namespace cvc5::kind;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -1036,4 +1036,4 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
index e6cfa31c6..a81f5f180 100644
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
@@ -22,7 +22,7 @@
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
 #include "theory/quantifiers/cegqi/vts_term_cache.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -209,6 +209,6 @@ class ArithInstantiator : public Instantiator
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index 2c163421e..bdd6d26ab 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -23,9 +23,9 @@
 #include "util/random.h"
 
 using namespace std;
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -759,4 +759,4 @@ void BvInstantiatorPreprocess::collectExtracts(
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
index 4bfda133e..9914428ef 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
@@ -21,7 +21,7 @@
 #include "theory/quantifiers/bv_inverter.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -209,6 +209,6 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
index 85faea4b1..030258113 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp
@@ -17,9 +17,9 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace utils {
@@ -342,4 +342,4 @@ Node normalizePvEqual(
 }  // namespace utils
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
index 576d68d06..ac68dc4d5 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
@@ -20,7 +20,7 @@
 #include "expr/attribute.h"
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -104,5 +104,5 @@ Node normalizePvEqual(
 }  // namespace utils
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 #endif
diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
index bb81d2790..672ed990a 100644
--- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
@@ -20,9 +20,9 @@
 #include "theory/datatypes/theory_datatypes_utils.h"
 
 using namespace std;
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -180,4 +180,4 @@ Node DtInstantiator::solve_dt(Node v, Node a, Node b, Node sa, Node sb)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
index c0386465d..27bf560cb 100644
--- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
@@ -20,7 +20,7 @@
 #include "expr/node.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -91,6 +91,6 @@ class DtInstantiator : public Instantiator
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 118c505fc..b9d70768b 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -32,9 +32,9 @@
 #include "theory/rewriter.h"
 
 using namespace std;
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -1638,4 +1638,4 @@ bool Instantiator::processEqualTerm(CegInstantiator* ci,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index 03161399c..986874266 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -23,7 +23,7 @@
 #include "theory/inference_id.h"
 #include "util/statistics_registry.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -822,6 +822,6 @@ class InstantiatorPreprocess
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index d6a504713..5e3a64325 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -26,10 +26,10 @@
 #include "theory/rewriter.h"
 
 using namespace std;
-using namespace CVC5::kind;
-using namespace CVC5::context;
+using namespace cvc5::kind;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -546,4 +546,4 @@ bool InstStrategyCegqi::processNestedQe(Node q, bool isPreregister)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index a5b79fb00..6d4ee047f 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -26,7 +26,7 @@
 #include "theory/quantifiers/quant_module.h"
 #include "util/statistics_registry.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -215,6 +215,6 @@ class InstStrategyCegqi : public QuantifiersModule
 
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp
index 9efc0ec31..d5fabbbd9 100644
--- a/src/theory/quantifiers/cegqi/nested_qe.cpp
+++ b/src/theory/quantifiers/cegqi/nested_qe.cpp
@@ -19,7 +19,7 @@
 #include "expr/subs.h"
 #include "theory/smt_engine_subsolver.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -152,4 +152,4 @@ Node NestedQe::doQe(Node q)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/cegqi/nested_qe.h b/src/theory/quantifiers/cegqi/nested_qe.h
index 29df5d16b..e0cccb9c9 100644
--- a/src/theory/quantifiers/cegqi/nested_qe.h
+++ b/src/theory/quantifiers/cegqi/nested_qe.h
@@ -23,7 +23,7 @@
 #include "context/cdhashmap.h"
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -81,6 +81,6 @@ class NestedQe
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
index 1a7431038..1974e7c7c 100644
--- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
@@ -19,9 +19,9 @@
 #include "theory/quantifiers/quantifiers_inference_manager.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -296,4 +296,4 @@ bool VtsTermCache::containsVtsInfinity(Node n, bool isFree)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.h b/src/theory/quantifiers/cegqi/vts_term_cache.h
index 53c198213..d56684d43 100644
--- a/src/theory/quantifiers/cegqi/vts_term_cache.h
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.h
@@ -21,7 +21,7 @@
 #include "expr/attribute.h"
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 /** Attribute to mark Skolems as virtual terms */
@@ -140,6 +140,6 @@ class VtsTermCache
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H */
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index ffe06a7ad..41d881f2c 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -26,13 +26,13 @@
 #include "theory/rewriter.h"
 #include "util/random.h"
 
-using namespace CVC5;
-using namespace CVC5::kind;
-using namespace CVC5::theory;
-using namespace CVC5::theory::quantifiers;
+using namespace cvc5;
+using namespace cvc5::kind;
+using namespace cvc5::theory;
+using namespace cvc5::theory::quantifiers;
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 
 struct sortConjectureScore {
   std::vector< int > d_scores;
@@ -2260,4 +2260,4 @@ unsigned ConjectureGenerator::optFullCheckFrequency() { return 1; }
 
 bool ConjectureGenerator::optStatsOnly() { return false; }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index cc3314f82..db609a521 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -23,7 +23,7 @@
 #include "theory/quantifiers/quant_module.h"
 #include "theory/type_enumerator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -466,6 +466,6 @@ private:  //information about ground equivalence classes
 
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp
index 6e7601072..fe712e01e 100644
--- a/src/theory/quantifiers/dynamic_rewrite.cpp
+++ b/src/theory/quantifiers/dynamic_rewrite.cpp
@@ -17,9 +17,9 @@
 #include "theory/rewriter.h"
 
 using namespace std;
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -183,4 +183,4 @@ Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h
index 79b4824b4..9fce59796 100644
--- a/src/theory/quantifiers/dynamic_rewrite.h
+++ b/src/theory/quantifiers/dynamic_rewrite.h
@@ -22,7 +22,7 @@
 #include "context/cdlist.h"
 #include "theory/uf/equality_engine.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -119,6 +119,6 @@ class DynamicRewriter
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 4c9da3632..a3708bdfe 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -24,9 +24,9 @@
 #include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -348,4 +348,4 @@ Node CandidateGeneratorSelector::getNextCandidate()
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h
index b21a96225..0de57f02f 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.h
+++ b/src/theory/quantifiers/ematching/candidate_generator.h
@@ -20,7 +20,7 @@
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -243,6 +243,6 @@ class CandidateGeneratorSelector : public CandidateGeneratorQE
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index 14f514b73..5a00d41ca 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -25,9 +25,9 @@
 #include "theory/uf/theory_uf_rewriter.h"
 #include "util/hash.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -526,4 +526,4 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas()
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h
index 66b374ea8..12c91be63 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.h
+++ b/src/theory/quantifiers/ematching/ho_trigger.h
@@ -25,7 +25,7 @@
 #include "theory/quantifiers/inst_match.h"
 #include "theory/quantifiers/ematching/trigger.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -275,6 +275,6 @@ class HigherOrderTrigger : public Trigger
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */
diff --git a/src/theory/quantifiers/ematching/im_generator.cpp b/src/theory/quantifiers/ematching/im_generator.cpp
index 2f415779a..9f24faf68 100644
--- a/src/theory/quantifiers/ematching/im_generator.cpp
+++ b/src/theory/quantifiers/ematching/im_generator.cpp
@@ -16,9 +16,9 @@
 
 #include "theory/quantifiers/ematching/trigger.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -36,4 +36,4 @@ bool IMGenerator::sendInstantiation(InstMatch& m, InferenceId id)
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h
index b0d937120..222e3c078 100644
--- a/src/theory/quantifiers/ematching/im_generator.h
+++ b/src/theory/quantifiers/ematching/im_generator.h
@@ -22,7 +22,7 @@
 #include "theory/inference_id.h"
 #include "theory/quantifiers/inst_match.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -117,6 +117,6 @@ protected:
 }  // namespace inst
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 79b6927f7..94e356418 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -29,9 +29,9 @@
 #include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -673,4 +673,4 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent,
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
index 32d6e38f1..7b440035f 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -22,7 +22,7 @@
 #include "theory/quantifiers/inst_match.h"
 #include "theory/quantifiers/ematching/im_generator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -325,6 +325,6 @@ class InstMatchGenerator : public IMGenerator {
 }  // namespace inst
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
index 6ac910e2e..6677a162f 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp
@@ -18,9 +18,9 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/uf/equality_engine_iterator.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -315,4 +315,4 @@ void InstMatchGeneratorMulti::processNewInstantiations(InstMatch& m,
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h
index 644a47bee..309aa2640 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h
@@ -23,7 +23,7 @@
 #include "theory/quantifiers/ematching/inst_match_generator.h"
 #include "theory/quantifiers/inst_match_trie.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -103,6 +103,6 @@ class InstMatchGeneratorMulti : public IMGenerator
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
index 94b7921ed..8289ea841 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp
@@ -17,9 +17,9 @@
 #include "theory/quantifiers/ematching/trigger_trie.h"
 #include "theory/quantifiers/term_util.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -175,4 +175,4 @@ int InstMatchGeneratorMultiLinear::getNextMatch(Node q, InstMatch& m)
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
index 00a372c8f..4d4339bac 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
@@ -22,7 +22,7 @@
 #include "expr/node.h"
 #include "theory/quantifiers/ematching/inst_match_generator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -85,6 +85,6 @@ class InstMatchGeneratorMultiLinear : public InstMatchGenerator
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
index 7d7b3e1c0..b6af066f8 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp
@@ -21,9 +21,9 @@
 #include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -198,4 +198,4 @@ int InstMatchGeneratorSimple::getActiveScore()
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
index 8361628da..ccc650044 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
@@ -23,7 +23,7 @@
 #include "expr/node_trie.h"
 #include "theory/quantifiers/ematching/inst_match_generator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -100,6 +100,6 @@ class InstMatchGeneratorSimple : public IMGenerator
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/ematching/inst_strategy.cpp b/src/theory/quantifiers/ematching/inst_strategy.cpp
index a56e7efeb..ad269ac31 100644
--- a/src/theory/quantifiers/ematching/inst_strategy.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy.cpp
@@ -16,7 +16,7 @@
 
 #include "theory/quantifiers/quantifiers_state.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -44,4 +44,4 @@ options::UserPatMode InstStrategy::getInstUserPatMode() const
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h
index 0537d92ce..1ce62f170 100644
--- a/src/theory/quantifiers/ematching/inst_strategy.h
+++ b/src/theory/quantifiers/ematching/inst_strategy.h
@@ -22,7 +22,7 @@
 #include "options/quantifiers_options.h"
 #include "theory/theory.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -85,6 +85,6 @@ class InstStrategy
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index c62a034e4..d298f994d 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -22,10 +22,10 @@
 #include "theory/quantifiers/quantifiers_state.h"
 #include "util/random.h"
 
-using namespace CVC5::kind;
-using namespace CVC5::theory::quantifiers::inst;
+using namespace cvc5::kind;
+using namespace cvc5::theory::quantifiers::inst;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -688,4 +688,4 @@ void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) {
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
index bc52d605c..2c765e194 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -21,7 +21,7 @@
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/quant_relevance.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -112,6 +112,6 @@ class InstStrategyAutoGenTriggers : public InstStrategy
 }; /* class InstStrategyAutoGenTriggers */
 }
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
index 4b0d619bc..12ad77ef2 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp
@@ -18,10 +18,10 @@
 #include "theory/quantifiers/ematching/trigger_database.h"
 #include "theory/quantifiers/quantifiers_state.h"
 
-using namespace CVC5::kind;
-using namespace CVC5::theory::quantifiers::inst;
+using namespace cvc5::kind;
+using namespace cvc5::theory::quantifiers::inst;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -175,4 +175,4 @@ void InstStrategyUserPatterns::addUserPattern(Node q, Node pat)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
index 1bb50af7b..ed247b89a 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
@@ -23,7 +23,7 @@
 #include "theory/quantifiers/ematching/inst_strategy.h"
 #include "theory/quantifiers/ematching/trigger.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -64,6 +64,6 @@ class InstStrategyUserPatterns : public InstStrategy
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 94054b8f9..86abb4986 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -23,11 +23,11 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_util.h"
 
-using namespace CVC5::kind;
-using namespace CVC5::context;
-using namespace CVC5::theory::quantifiers::inst;
+using namespace cvc5::kind;
+using namespace cvc5::context;
+using namespace cvc5::theory::quantifiers::inst;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -272,4 +272,4 @@ bool InstantiationEngine::shouldProcess(Node q)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index 8dface27e..bd7388afb 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -24,7 +24,7 @@
 #include "theory/quantifiers/quant_module.h"
 #include "theory/quantifiers/quant_relevance.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -75,6 +75,6 @@ class InstantiationEngine : public QuantifiersModule {
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */
diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp
index 467ed46be..fb5bd49a3 100644
--- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp
+++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp
@@ -20,9 +20,9 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -729,4 +729,4 @@ void PatternTermSelector::getTriggerVariables(Node n,
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.h b/src/theory/quantifiers/ematching/pattern_term_selector.h
index 6f26f2cec..5ac6c1da3 100644
--- a/src/theory/quantifiers/ematching/pattern_term_selector.h
+++ b/src/theory/quantifiers/ematching/pattern_term_selector.h
@@ -23,7 +23,7 @@
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/ematching/trigger_term_info.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -192,6 +192,6 @@ class PatternTermSelector
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index 234940b54..dd0af2e18 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -32,9 +32,9 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/valuation.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -229,4 +229,4 @@ void Trigger::debugPrint(const char* c) const
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index c6d3b3cd5..e2ad00561 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -20,7 +20,7 @@
 #include "expr/node.h"
 #include "theory/inference_id.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 class QuantifiersEngine;
@@ -219,6 +219,6 @@ class Trigger {
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_H */
diff --git a/src/theory/quantifiers/ematching/trigger_database.cpp b/src/theory/quantifiers/ematching/trigger_database.cpp
index 327d2bba1..fa8d2ff52 100644
--- a/src/theory/quantifiers/ematching/trigger_database.cpp
+++ b/src/theory/quantifiers/ematching/trigger_database.cpp
@@ -18,7 +18,7 @@
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/term_util.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -185,4 +185,4 @@ bool TriggerDatabase::mkTriggerTerms(Node q,
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/trigger_database.h b/src/theory/quantifiers/ematching/trigger_database.h
index 2c28c77bc..9cebb6173 100644
--- a/src/theory/quantifiers/ematching/trigger_database.h
+++ b/src/theory/quantifiers/ematching/trigger_database.h
@@ -22,7 +22,7 @@
 #include "expr/node.h"
 #include "theory/quantifiers/ematching/trigger_trie.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -105,6 +105,6 @@ class TriggerDatabase
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H */
diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp
index 1f3ca0577..984e825f0 100644
--- a/src/theory/quantifiers/ematching/trigger_term_info.cpp
+++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp
@@ -16,9 +16,9 @@
 
 #include "theory/quantifiers/term_util.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -114,4 +114,4 @@ int32_t TriggerTermInfo::getTriggerWeight(Node n)
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/trigger_term_info.h b/src/theory/quantifiers/ematching/trigger_term_info.h
index 603a1ab77..c70257e08 100644
--- a/src/theory/quantifiers/ematching/trigger_term_info.h
+++ b/src/theory/quantifiers/ematching/trigger_term_info.h
@@ -21,7 +21,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -124,6 +124,6 @@ class TriggerTermInfo
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/ematching/trigger_trie.cpp b/src/theory/quantifiers/ematching/trigger_trie.cpp
index c8a13d447..7ca925b53 100644
--- a/src/theory/quantifiers/ematching/trigger_trie.cpp
+++ b/src/theory/quantifiers/ematching/trigger_trie.cpp
@@ -14,7 +14,7 @@
 
 #include "theory/quantifiers/ematching/trigger_trie.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -74,4 +74,4 @@ void TriggerTrie::addTrigger(std::vector<Node>& nodes, inst::Trigger* t)
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/trigger_trie.h b/src/theory/quantifiers/ematching/trigger_trie.h
index 355ad6c31..fe16e3c0f 100644
--- a/src/theory/quantifiers/ematching/trigger_trie.h
+++ b/src/theory/quantifiers/ematching/trigger_trie.h
@@ -22,7 +22,7 @@
 #include "expr/node.h"
 #include "theory/quantifiers/ematching/trigger.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -58,6 +58,6 @@ class TriggerTrie
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H */
diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp
index e2dd3f37d..63a9cceae 100644
--- a/src/theory/quantifiers/ematching/var_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/var_match_generator.cpp
@@ -16,9 +16,9 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -81,4 +81,4 @@ int VarMatchGeneratorTermSubs::getNextMatch(Node q, InstMatch& m)
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h
index 6ee179e91..87c4d1e32 100644
--- a/src/theory/quantifiers/ematching/var_match_generator.h
+++ b/src/theory/quantifiers/ematching/var_match_generator.h
@@ -20,7 +20,7 @@
 #include "expr/node.h"
 #include "theory/quantifiers/ematching/inst_match_generator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace inst {
@@ -53,6 +53,6 @@ class VarMatchGeneratorTermSubs : public InstMatchGenerator
 }  // namespace inst
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index 7846a60bd..77b402843 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -21,10 +21,10 @@
 #include "theory/quantifiers/term_util.h"
 
 using namespace std;
-using namespace CVC5::kind;
-using namespace CVC5::context;
+using namespace cvc5::kind;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -187,4 +187,4 @@ int32_t EqualityQuery::getRepScore(Node n, Node q, size_t index, TypeNode v_tn)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
index d863c830b..988291ed5 100644
--- a/src/theory/quantifiers/equality_query.h
+++ b/src/theory/quantifiers/equality_query.h
@@ -22,7 +22,7 @@
 #include "expr/node.h"
 #include "theory/quantifiers/quant_util.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -90,6 +90,6 @@ class EqualityQuery : public QuantifiersUtil
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 20f3afe63..b21252358 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -22,9 +22,9 @@
 #include "theory/smt_engine_subsolver.h"
 
 using namespace std;
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -104,4 +104,4 @@ Result ExprMiner::doCheck(Node query)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index 7046dad83..37d0de6f8 100644
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -25,7 +25,7 @@
 #include "smt/smt_engine.h"
 #include "theory/quantifiers/sygus_sampler.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -90,6 +90,6 @@ class ExprMiner
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H */
diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp
index 867e6748a..b84968adf 100644
--- a/src/theory/quantifiers/expr_miner_manager.cpp
+++ b/src/theory/quantifiers/expr_miner_manager.cpp
@@ -16,7 +16,7 @@
 
 #include "options/quantifiers_options.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -165,4 +165,4 @@ bool ExpressionMinerManager::addTerm(Node sol, std::ostream& out)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h
index 6e775f586..d33c9902c 100644
--- a/src/theory/quantifiers/expr_miner_manager.h
+++ b/src/theory/quantifiers/expr_miner_manager.h
@@ -24,7 +24,7 @@
 #include "theory/quantifiers/solution_filter.h"
 #include "theory/quantifiers/sygus_sampler.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 class QuantifiersEngine;
@@ -118,6 +118,6 @@ class ExpressionMinerManager
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H */
diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 01d573607..092041b15 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -24,10 +24,10 @@
 #include "theory/strings/sequences_rewriter.h"
 #include "theory/theory.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -1726,4 +1726,4 @@ void ExtendedRewriter::debugExtendedRewrite(Node n,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index f04f9eaae..0d6ece71e 100644
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -21,7 +21,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -250,6 +250,6 @@ class ExtendedRewriter
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index bbd6443fa..eb1e4e96a 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -23,10 +23,10 @@
 #include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
 
-using namespace CVC5::kind;
-using namespace CVC5::context;
+using namespace cvc5::kind;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -363,4 +363,4 @@ unsigned FirstOrderModel::getModelBasisArg(Node n)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 7a578a33a..ec3b6dd7a 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -22,7 +22,7 @@
 #include "theory/theory_model.h"
 #include "theory/uf/theory_uf_model.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 class QuantifiersEngine;
@@ -196,6 +196,6 @@ class FirstOrderModel : public TheoryModel
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__FIRST_ORDER_MODEL_H */
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 6044de049..efa3dd160 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -28,11 +28,11 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5;
+using namespace cvc5;
 using namespace std;
-using namespace CVC5::theory;
-using namespace CVC5::theory::quantifiers;
-using namespace CVC5::kind;
+using namespace cvc5::theory;
+using namespace cvc5::theory::quantifiers;
+using namespace cvc5::kind;
 
 BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic(
     Node r,
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index f2abf743a..fc6fac92a 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -26,7 +26,7 @@
 #include "theory/decision_strategy.h"
 #include "theory/quantifiers/quant_bound_inference.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 class RepSetIterator;
@@ -238,6 +238,6 @@ private:
 
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
index 7c9aacd76..515d9fe58 100644
--- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
@@ -18,9 +18,9 @@
 #include "theory/quantifiers/fmf/full_model_check.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace fmcheck {
@@ -156,4 +156,4 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix)
 }  // namespace fmcheck
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.h b/src/theory/quantifiers/fmf/first_order_model_fmc.h
index 86665aef4..d858e24f6 100644
--- a/src/theory/quantifiers/fmf/first_order_model_fmc.h
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.h
@@ -19,7 +19,7 @@
 
 #include "theory/quantifiers/first_order_model.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace fmcheck {
@@ -54,6 +54,6 @@ class FirstOrderModelFmc : public FirstOrderModel
 }  // namespace fmcheck
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__FIRST_ORDER_MODEL_H */
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 3a7209f00..7dbc10f57 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -28,10 +28,10 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
-using namespace CVC5::context;
+using namespace cvc5::kind;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace fmcheck {
@@ -1375,4 +1375,4 @@ bool FullModelChecker::isHandled(Node q) const
 }  // namespace fmcheck
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index 19ecc8ddc..586bde226 100644
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -20,7 +20,7 @@
 #include "theory/quantifiers/fmf/first_order_model_fmc.h"
 #include "theory/quantifiers/fmf/model_builder.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 namespace fmcheck {
@@ -187,6 +187,6 @@ protected:
 }  // namespace fmcheck
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index 17935f6b4..27eed53f2 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -22,11 +22,11 @@
 #include "theory/quantifiers/quantifiers_state.h"
 
 using namespace std;
-using namespace CVC5;
-using namespace CVC5::kind;
-using namespace CVC5::context;
-using namespace CVC5::theory;
-using namespace CVC5::theory::quantifiers;
+using namespace cvc5;
+using namespace cvc5::kind;
+using namespace cvc5::context;
+using namespace cvc5::theory;
+using namespace cvc5::theory::quantifiers;
 
 QModelBuilder::QModelBuilder(QuantifiersState& qs,
                              QuantifiersRegistry& qr,
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index 2b102c0a8..4a95a8a73 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -21,7 +21,7 @@
 #include "theory/quantifiers/inst_match.h"
 #include "theory/theory_model_builder.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -73,6 +73,6 @@ class QModelBuilder : public TheoryEngineModelBuilder
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H */
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 9943744f7..1c46e425d 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -22,10 +22,10 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/term_database.h"
 
-using namespace CVC5::kind;
-using namespace CVC5::context;
+using namespace cvc5::kind;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -343,4 +343,4 @@ void ModelEngine::debugPrint( const char* c ){
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h
index 078894de6..2547f2831 100644
--- a/src/theory/quantifiers/fmf/model_engine.h
+++ b/src/theory/quantifiers/fmf/model_engine.h
@@ -21,7 +21,7 @@
 #include "theory/quantifiers/quant_module.h"
 #include "theory/theory_model.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -71,6 +71,6 @@ private:
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H */
diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp
index 326de79fa..9a3d465d5 100644
--- a/src/theory/quantifiers/fun_def_evaluator.cpp
+++ b/src/theory/quantifiers/fun_def_evaluator.cpp
@@ -19,9 +19,9 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -252,4 +252,4 @@ bool FunDefEvaluator::hasDefinitions() const { return !d_funDefMap.empty(); }
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/fun_def_evaluator.h b/src/theory/quantifiers/fun_def_evaluator.h
index be4070840..fcc30948d 100644
--- a/src/theory/quantifiers/fun_def_evaluator.h
+++ b/src/theory/quantifiers/fun_def_evaluator.h
@@ -22,7 +22,7 @@
 #include "expr/node.h"
 #include "theory/evaluator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -70,6 +70,6 @@ class FunDefEvaluator
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/index_trie.cpp b/src/theory/quantifiers/index_trie.cpp
index 444882729..8c00efb0e 100644
--- a/src/theory/quantifiers/index_trie.cpp
+++ b/src/theory/quantifiers/index_trie.cpp
@@ -15,7 +15,7 @@
  **/
 #include "theory/quantifiers/index_trie.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -114,4 +114,4 @@ IndexTrieNode* IndexTrie::addRec(IndexTrieNode* n,
 }
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/index_trie.h b/src/theory/quantifiers/index_trie.h
index 4ac754252..2c968e107 100644
--- a/src/theory/quantifiers/index_trie.h
+++ b/src/theory/quantifiers/index_trie.h
@@ -21,7 +21,7 @@
 
 #include "base/check.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -106,5 +106,5 @@ class IndexTrie
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 #endif /* THEORY__QUANTIFIERS__INDEX_TRIE_H */
diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 3db8db74e..c2f65ea93 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -16,7 +16,7 @@
 
 #include "theory/quantifiers/quantifiers_state.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -102,4 +102,4 @@ bool InstMatch::set(QuantifiersState& qs, size_t i, TNode n)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 9ff507917..e5e8f97cd 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -21,7 +21,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -89,6 +89,6 @@ inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */
diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp
index 879eb8479..347fe45af 100644
--- a/src/theory/quantifiers/inst_match_trie.cpp
+++ b/src/theory/quantifiers/inst_match_trie.cpp
@@ -20,9 +20,9 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/uf/equality_engine_iterator.h"
 
-using namespace CVC5::context;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -369,4 +369,4 @@ bool InstMatchTrieOrdered::existsInstMatch(quantifiers::QuantifiersState& qs,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h
index da8858e8a..ca878c888 100644
--- a/src/theory/quantifiers/inst_match_trie.h
+++ b/src/theory/quantifiers/inst_match_trie.h
@@ -23,7 +23,7 @@
 #include "context/cdo.h"
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -224,6 +224,6 @@ class InstMatchTrieOrdered
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H */
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index c2ee94d1e..3e560acaa 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -21,10 +21,10 @@
 #include "theory/quantifiers/term_tuple_enumerator.h"
 #include "theory/quantifiers/term_util.h"
 
-using namespace CVC5::kind;
-using namespace CVC5::context;
+using namespace cvc5::kind;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -220,4 +220,4 @@ bool InstStrategyEnum::process(Node quantifier, bool fullEffort, bool isRd)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index 05e5f7352..7b5cb8e0e 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -19,7 +19,7 @@
 
 #include "theory/quantifiers/quant_module.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -116,6 +116,6 @@ class InstStrategyEnum : public QuantifiersModule
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 4f878c79b..62376bff6 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -33,10 +33,10 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
-using namespace CVC5::context;
+using namespace cvc5::kind;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -760,4 +760,4 @@ Instantiate::Statistics::~Statistics()
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 3fb194589..b3c056506 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -27,7 +27,7 @@
 #include "theory/quantifiers/quant_util.h"
 #include "util/statistics_registry.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 class LazyCDProof;
 
@@ -361,6 +361,6 @@ class Instantiate : public QuantifiersUtil
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */
diff --git a/src/theory/quantifiers/instantiation_list.cpp b/src/theory/quantifiers/instantiation_list.cpp
index 1c3a0bcac..78bfdf9a4 100644
--- a/src/theory/quantifiers/instantiation_list.cpp
+++ b/src/theory/quantifiers/instantiation_list.cpp
@@ -17,7 +17,7 @@
 #include "options/base_options.h"
 #include "printer/printer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 std::ostream& operator<<(std::ostream& out, const InstantiationList& ilist)
 {
@@ -31,4 +31,4 @@ std::ostream& operator<<(std::ostream& out, const SkolemList& skl)
   return out;
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/instantiation_list.h b/src/theory/quantifiers/instantiation_list.h
index da8d5c3b5..86dfa0081 100644
--- a/src/theory/quantifiers/instantiation_list.h
+++ b/src/theory/quantifiers/instantiation_list.h
@@ -22,7 +22,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 /** A list of instantiations for a quantified formula */
 struct InstantiationList
@@ -53,6 +53,6 @@ struct SkolemList
 /** Print the skolem list to stream out */
 std::ostream& operator<<(std::ostream& out, const SkolemList& skl);
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H */
diff --git a/src/theory/quantifiers/kinds b/src/theory/quantifiers/kinds
index 6a32969e3..4561226e1 100644
--- a/src/theory/quantifiers/kinds
+++ b/src/theory/quantifiers/kinds
@@ -4,12 +4,12 @@
 # src/theory/builtin/kinds.
 #
 
-theory THEORY_QUANTIFIERS ::CVC5::theory::quantifiers::TheoryQuantifiers "theory/quantifiers/theory_quantifiers.h"
+theory THEORY_QUANTIFIERS ::cvc5::theory::quantifiers::TheoryQuantifiers "theory/quantifiers/theory_quantifiers.h"
 typechecker "theory/quantifiers/theory_quantifiers_type_rules.h"
 
 properties check presolve
 
-rewriter ::CVC5::theory::quantifiers::QuantifiersRewriter "theory/quantifiers/quantifiers_rewriter.h"
+rewriter ::cvc5::theory::quantifiers::QuantifiersRewriter "theory/quantifiers/quantifiers_rewriter.h"
 
 operator FORALL 2:3 "universally quantified formula; first parameter is an BOUND_VAR_LIST, second is quantifier body, and an optional third parameter is an INST_PATTERN_LIST"
 
@@ -47,16 +47,16 @@ sort INST_PATTERN_LIST_TYPE \
 # a list of instantiation patterns
 operator INST_PATTERN_LIST 1: "a list of instantiation patterns"
 
-typerule FORALL ::CVC5::theory::quantifiers::QuantifierTypeRule
-typerule EXISTS ::CVC5::theory::quantifiers::QuantifierTypeRule
-typerule BOUND_VAR_LIST ::CVC5::theory::quantifiers::QuantifierBoundVarListTypeRule
-typerule INST_PATTERN_LIST ::CVC5::theory::quantifiers::QuantifierInstPatternListTypeRule
-
-typerule INST_PATTERN ::CVC5::theory::quantifiers::QuantifierInstPatternTypeRule
-typerule INST_NO_PATTERN ::CVC5::theory::quantifiers::QuantifierAnnotationTypeRule
-typerule INST_ATTRIBUTE ::CVC5::theory::quantifiers::QuantifierAnnotationTypeRule
-typerule INST_POOL ::CVC5::theory::quantifiers::QuantifierAnnotationTypeRule
-typerule INST_ADD_TO_POOL ::CVC5::theory::quantifiers::QuantifierAnnotationTypeRule
-typerule SKOLEM_ADD_TO_POOL ::CVC5::theory::quantifiers::QuantifierAnnotationTypeRule
+typerule FORALL ::cvc5::theory::quantifiers::QuantifierTypeRule
+typerule EXISTS ::cvc5::theory::quantifiers::QuantifierTypeRule
+typerule BOUND_VAR_LIST ::cvc5::theory::quantifiers::QuantifierBoundVarListTypeRule
+typerule INST_PATTERN_LIST ::cvc5::theory::quantifiers::QuantifierInstPatternListTypeRule
+
+typerule INST_PATTERN ::cvc5::theory::quantifiers::QuantifierInstPatternTypeRule
+typerule INST_NO_PATTERN ::cvc5::theory::quantifiers::QuantifierAnnotationTypeRule
+typerule INST_ATTRIBUTE ::cvc5::theory::quantifiers::QuantifierAnnotationTypeRule
+typerule INST_POOL ::cvc5::theory::quantifiers::QuantifierAnnotationTypeRule
+typerule INST_ADD_TO_POOL ::cvc5::theory::quantifiers::QuantifierAnnotationTypeRule
+typerule SKOLEM_ADD_TO_POOL ::cvc5::theory::quantifiers::QuantifierAnnotationTypeRule
 
 endtheory
diff --git a/src/theory/quantifiers/lazy_trie.cpp b/src/theory/quantifiers/lazy_trie.cpp
index 1b706d904..06d1798d5 100644
--- a/src/theory/quantifiers/lazy_trie.cpp
+++ b/src/theory/quantifiers/lazy_trie.cpp
@@ -14,7 +14,7 @@
 
 #include "theory/quantifiers/lazy_trie.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -156,4 +156,4 @@ void LazyTrieMulti::clear()
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h
index 2d92b13fd..d4437ae75 100644
--- a/src/theory/quantifiers/lazy_trie.h
+++ b/src/theory/quantifiers/lazy_trie.h
@@ -17,7 +17,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -168,6 +168,6 @@ class LazyTrieMulti
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H */
diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp
index 572c631e1..4be66a703 100644
--- a/src/theory/quantifiers/proof_checker.cpp
+++ b/src/theory/quantifiers/proof_checker.cpp
@@ -18,9 +18,9 @@
 #include "expr/skolem_manager.h"
 #include "theory/builtin/proof_checker.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -123,4 +123,4 @@ Node QuantifiersProofRuleChecker::checkInternal(
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/proof_checker.h b/src/theory/quantifiers/proof_checker.h
index da78daf90..39e933149 100644
--- a/src/theory/quantifiers/proof_checker.h
+++ b/src/theory/quantifiers/proof_checker.h
@@ -21,7 +21,7 @@
 #include "expr/proof_checker.h"
 #include "expr/proof_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -44,6 +44,6 @@ class QuantifiersProofRuleChecker : public ProofRuleChecker
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__PROOF_CHECKER_H */
diff --git a/src/theory/quantifiers/quant_bound_inference.cpp b/src/theory/quantifiers/quant_bound_inference.cpp
index 6d7e2e9cd..609bc66a4 100644
--- a/src/theory/quantifiers/quant_bound_inference.cpp
+++ b/src/theory/quantifiers/quant_bound_inference.cpp
@@ -17,9 +17,9 @@
 #include "theory/quantifiers/fmf/bounded_integers.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -127,4 +127,4 @@ bool QuantifiersBoundInference::getBoundElements(
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/quant_bound_inference.h b/src/theory/quantifiers/quant_bound_inference.h
index 62ac0ea58..7c15d5146 100644
--- a/src/theory/quantifiers/quant_bound_inference.h
+++ b/src/theory/quantifiers/quant_bound_inference.h
@@ -20,7 +20,7 @@
 #include <vector>
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 class RepSetIterator;
@@ -122,6 +122,6 @@ class QuantifiersBoundInference
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H */
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 5fa617670..94b2f001e 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -29,10 +29,10 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -2351,4 +2351,4 @@ bool QuantConflictFind::isPropagatingInstance(Node n) const
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index ef605a48a..93e6075a8 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -25,7 +25,7 @@
 #include "expr/node_trie.h"
 #include "theory/quantifiers/quant_module.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -313,6 +313,6 @@ std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e);
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp
index 811dc8642..2c74b3557 100644
--- a/src/theory/quantifiers/quant_module.cpp
+++ b/src/theory/quantifiers/quant_module.cpp
@@ -14,9 +14,9 @@
 
 #include "theory/quantifiers/quant_module.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 QuantifiersModule::QuantifiersModule(
@@ -75,4 +75,4 @@ quantifiers::QuantifiersRegistry& QuantifiersModule::getQuantifiersRegistry()
 }
 
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h
index 53fb55aa0..e6d5eee76 100644
--- a/src/theory/quantifiers/quant_module.h
+++ b/src/theory/quantifiers/quant_module.h
@@ -28,7 +28,7 @@
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 class TermDb;
@@ -174,6 +174,6 @@ class QuantifiersModule
 }; /* class QuantifiersModule */
 
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANT_UTIL_H */
diff --git a/src/theory/quantifiers/quant_relevance.cpp b/src/theory/quantifiers/quant_relevance.cpp
index 2ce79d285..f6a96cda2 100644
--- a/src/theory/quantifiers/quant_relevance.cpp
+++ b/src/theory/quantifiers/quant_relevance.cpp
@@ -15,10 +15,10 @@
 #include "theory/quantifiers/quant_relevance.h"
 
 using namespace std;
-using namespace CVC5::kind;
-using namespace CVC5::context;
+using namespace cvc5::kind;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -62,4 +62,4 @@ size_t QuantRelevance::getNumQuantifiersForSymbol(Node s) const
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h
index 73b62489e..e6a178c73 100644
--- a/src/theory/quantifiers/quant_relevance.h
+++ b/src/theory/quantifiers/quant_relevance.h
@@ -21,7 +21,7 @@
 
 #include "theory/quantifiers/quant_util.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -63,6 +63,6 @@ class QuantRelevance : public QuantifiersUtil
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANT_RELEVANCE_H */
diff --git a/src/theory/quantifiers/quant_rep_bound_ext.cpp b/src/theory/quantifiers/quant_rep_bound_ext.cpp
index 2a70e5d4e..383091e33 100644
--- a/src/theory/quantifiers/quant_rep_bound_ext.cpp
+++ b/src/theory/quantifiers/quant_rep_bound_ext.cpp
@@ -17,9 +17,9 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quant_bound_inference.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -86,4 +86,4 @@ bool QRepBoundExt::getVariableOrder(Node owner, std::vector<unsigned>& varOrder)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/quant_rep_bound_ext.h b/src/theory/quantifiers/quant_rep_bound_ext.h
index 7e8f5d386..6fe0faefa 100644
--- a/src/theory/quantifiers/quant_rep_bound_ext.h
+++ b/src/theory/quantifiers/quant_rep_bound_ext.h
@@ -23,7 +23,7 @@
 #include "theory/rep_set.h"
 #include "theory/theory_model.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -67,6 +67,6 @@ class QRepBoundExt : public RepBoundExt
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__FIRST_ORDER_MODEL_H */
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 85fb291f0..00a8ff08f 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -20,9 +20,9 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "options/quantifiers_options.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -207,4 +207,4 @@ void QuantDSplit::check(Theory::Effort e, QEffort quant_e)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index eb85a2c28..ee961cbbc 100644
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -20,7 +20,7 @@
 #include "context/cdo.h"
 #include "theory/quantifiers/quant_module.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 class QuantifiersEngine;
@@ -73,6 +73,6 @@ class QuantDSplit : public QuantifiersModule {
 
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 841778a89..cbf29065c 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -16,9 +16,9 @@
 
 #include "theory/quantifiers/term_util.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
@@ -131,4 +131,4 @@ void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol,
 }
 
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index f41f394e8..7cd89c7d8 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -24,7 +24,7 @@
 #include "expr/node.h"
 #include "theory/theory.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 /** Quantifiers utility
@@ -78,6 +78,6 @@ public:
 };
 
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANT_UTIL_H */
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 8c068e06c..d53ed74be 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -20,10 +20,10 @@
 #include "theory/quantifiers/term_util.h"
 
 using namespace std;
-using namespace CVC5::kind;
-using namespace CVC5::context;
+using namespace cvc5::kind;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -378,4 +378,4 @@ void QuantAttributes::setInstantiationLevelAttr(Node n, uint64_t level)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 4f7f1e22c..2fb294abe 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -22,7 +22,7 @@
 #include "expr/attribute.h"
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 /** Attribute true for function definition quantifiers */
@@ -244,6 +244,6 @@ class QuantAttributes
 
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp
index 687e17e4a..ff3087b63 100644
--- a/src/theory/quantifiers/quantifiers_inference_manager.cpp
+++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp
@@ -17,7 +17,7 @@
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/skolemize.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -53,4 +53,4 @@ void QuantifiersInferenceManager::doPending()
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h
index afe8dd40a..b468e0478 100644
--- a/src/theory/quantifiers/quantifiers_inference_manager.h
+++ b/src/theory/quantifiers/quantifiers_inference_manager.h
@@ -20,7 +20,7 @@
 #include "theory/inference_manager_buffered.h"
 #include "theory/quantifiers/quantifiers_state.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -59,6 +59,6 @@ class QuantifiersInferenceManager : public InferenceManagerBuffered
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H */
diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index e39e38ea7..049e72edf 100644
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -18,7 +18,7 @@
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/term_registry.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -122,4 +122,4 @@ void QuantifiersModules::initialize(QuantifiersState& qs,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h
index 71928502d..c52da79a7 100644
--- a/src/theory/quantifiers/quantifiers_modules.h
+++ b/src/theory/quantifiers/quantifiers_modules.h
@@ -30,7 +30,7 @@
 #include "theory/quantifiers/sygus/synth_engine.h"
 #include "theory/quantifiers/sygus_inst.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
   
 class QuantifiersEngine;
@@ -45,7 +45,7 @@ namespace quantifiers {
  */
 class QuantifiersModules
 {
-  friend class ::CVC5::theory::QuantifiersEngine;
+  friend class ::cvc5::theory::QuantifiersEngine;
 
  public:
   QuantifiersModules();
@@ -94,6 +94,6 @@ class QuantifiersModules
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H */
diff --git a/src/theory/quantifiers/quantifiers_registry.cpp b/src/theory/quantifiers/quantifiers_registry.cpp
index 3cd59c834..58edc72bd 100644
--- a/src/theory/quantifiers/quantifiers_registry.cpp
+++ b/src/theory/quantifiers/quantifiers_registry.cpp
@@ -18,7 +18,7 @@
 #include "theory/quantifiers/quant_module.h"
 #include "theory/quantifiers/term_util.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -208,4 +208,4 @@ bool QuantifiersRegistry::getNameForQuant(Node q, Node& name, bool req) const
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h
index a3dffb063..383934c15 100644
--- a/src/theory/quantifiers/quantifiers_registry.h
+++ b/src/theory/quantifiers/quantifiers_registry.h
@@ -22,7 +22,7 @@
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 class QuantifiersModule;
@@ -129,6 +129,6 @@ class QuantifiersRegistry : public QuantifiersUtil
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index d31b22f88..2c91df7a7 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -32,10 +32,10 @@
 #include "theory/strings/theory_strings_utils.h"
 
 using namespace std;
-using namespace CVC5::kind;
-using namespace CVC5::context;
+using namespace cvc5::kind;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -2030,4 +2030,4 @@ TrustNode QuantifiersRewriter::preprocess(Node n, bool isInst)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 7bbe32da7..5ea8352d0 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -22,7 +22,7 @@
 #include "theory/theory_rewriter.h"
 #include "theory/trust_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -303,6 +303,6 @@ public:
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */
diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp
index 5e3bb3ba3..927369442 100644
--- a/src/theory/quantifiers/quantifiers_state.cpp
+++ b/src/theory/quantifiers/quantifiers_state.cpp
@@ -17,7 +17,7 @@
 #include "options/quantifiers_options.h"
 #include "theory/uf/equality_engine_iterator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -160,4 +160,4 @@ QuantifiersStatistics& QuantifiersState::getStats() { return d_statistics; }
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h
index 0f1c13659..623d52289 100644
--- a/src/theory/quantifiers/quantifiers_state.h
+++ b/src/theory/quantifiers/quantifiers_state.h
@@ -21,7 +21,7 @@
 #include "theory/theory.h"
 #include "theory/theory_state.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -86,6 +86,6 @@ class QuantifiersState : public TheoryState
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H */
diff --git a/src/theory/quantifiers/quantifiers_statistics.cpp b/src/theory/quantifiers/quantifiers_statistics.cpp
index e922c7080..720ae2ee0 100644
--- a/src/theory/quantifiers/quantifiers_statistics.cpp
+++ b/src/theory/quantifiers/quantifiers_statistics.cpp
@@ -16,7 +16,7 @@
 
 #include "smt/smt_statistics_registry.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -61,4 +61,4 @@ QuantifiersStatistics::~QuantifiersStatistics()
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/quantifiers_statistics.h b/src/theory/quantifiers/quantifiers_statistics.h
index 9f2678796..9eccf3ce6 100644
--- a/src/theory/quantifiers/quantifiers_statistics.h
+++ b/src/theory/quantifiers/quantifiers_statistics.h
@@ -20,7 +20,7 @@
 #include "util/statistics_registry.h"
 #include "util/stats_timer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -47,6 +47,6 @@ class QuantifiersStatistics
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H */
diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp
index 0860549ba..6abb8bbec 100644
--- a/src/theory/quantifiers/query_generator.cpp
+++ b/src/theory/quantifiers/query_generator.cpp
@@ -24,9 +24,9 @@
 #include "util/random.h"
 
 using namespace std;
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -425,4 +425,4 @@ void QueryGenerator::findQueries(
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h
index a847a184b..cf10b42da 100644
--- a/src/theory/quantifiers/query_generator.h
+++ b/src/theory/quantifiers/query_generator.h
@@ -25,7 +25,7 @@
 #include "theory/quantifiers/lazy_trie.h"
 #include "theory/quantifiers/sygus_sampler.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -116,6 +116,6 @@ class QueryGenerator : public ExprMiner
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS___H */
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 3e25f4073..6fb27bec4 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -22,9 +22,9 @@
 #include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -338,4 +338,4 @@ void RelevantDomain::computeRelevantDomainLit( Node q, bool hasPol, bool pol, No
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 56b728b34..807e4c4a2 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -20,7 +20,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quant_util.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -170,6 +170,6 @@ class RelevantDomain : public QuantifiersUtil
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */
diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp
index 1dbc24280..2fe173763 100644
--- a/src/theory/quantifiers/single_inv_partition.cpp
+++ b/src/theory/quantifiers/single_inv_partition.cpp
@@ -20,11 +20,11 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5;
-using namespace CVC5::kind;
+using namespace cvc5;
+using namespace cvc5::kind;
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -615,4 +615,4 @@ void SingleInvocationPartition::debugPrint(const char* c)
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h
index 6feff4169..604c711ad 100644
--- a/src/theory/quantifiers/single_inv_partition.h
+++ b/src/theory/quantifiers/single_inv_partition.h
@@ -23,7 +23,7 @@
 #include "expr/node.h"
 #include "expr/type_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -292,6 +292,6 @@ class SingleInvocationPartition
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index 3767fac61..2a19824ac 100644
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -27,9 +27,9 @@
 #include "theory/rewriter.h"
 #include "theory/sort_inference.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -399,4 +399,4 @@ bool Skolemize::isProofEnabled() const { return d_epg != nullptr; }
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index d0a889ace..4c4d770f3 100644
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -26,7 +26,7 @@
 #include "theory/eager_proof_generator.h"
 #include "theory/trust_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 class DTypeConstructor;
 
@@ -157,6 +157,6 @@ class Skolemize
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H */
diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp
index 3b00f5081..d7556be40 100644
--- a/src/theory/quantifiers/solution_filter.cpp
+++ b/src/theory/quantifiers/solution_filter.cpp
@@ -20,9 +20,9 @@
 #include "smt/smt_engine_scope.h"
 #include "util/random.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -103,4 +103,4 @@ bool SolutionFilterStrength::addTerm(Node n, std::ostream& out)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/solution_filter.h b/src/theory/quantifiers/solution_filter.h
index cea5eb74e..bf3d9bddc 100644
--- a/src/theory/quantifiers/solution_filter.h
+++ b/src/theory/quantifiers/solution_filter.h
@@ -24,7 +24,7 @@
 #include "theory/quantifiers/lazy_trie.h"
 #include "theory/quantifiers/sygus_sampler.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -70,6 +70,6 @@ class SolutionFilterStrength : public ExprMiner
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H */
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index 0acd7e718..5e9f2d591 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -32,9 +32,9 @@
 #include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -548,4 +548,4 @@ bool CegSingleInv::solveTrivial(Node q)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index e2f399ffd..ca83bf973 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -24,7 +24,7 @@
 #include "theory/quantifiers/single_inv_partition.h"
 #include "theory/quantifiers/sygus/sygus_stats.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -178,6 +178,6 @@ class CegSingleInv
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index d980db887..52adc1972 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -24,10 +24,10 @@
 #include "theory/rewriter.h"
 
 using namespace std;
-using namespace CVC5::kind;
-using namespace CVC5::context;
+using namespace cvc5::kind;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -706,4 +706,4 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index a12133d23..f728d3d7e 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -21,7 +21,7 @@
 #include "theory/quantifiers/sygus/sygus_module.h"
 #include "theory/quantifiers/sygus_sampler.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -227,6 +227,6 @@ class Cegis : public SygusModule
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__CEGIS_H */
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index 26ad62c90..6e47c2d89 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -28,9 +28,9 @@
 #include "theory/smt_engine_subsolver.h"
 #include "util/random.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -861,4 +861,4 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h
index 59bf53317..2abce835a 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.h
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.h
@@ -25,7 +25,7 @@
 #include "theory/quantifiers/sygus/cegis.h"
 #include "util/result.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 class SmtEngine;
 
@@ -399,6 +399,6 @@ class CegisCoreConnective : public Cegis
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index bcd9fa67a..9a5c6146d 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -21,9 +21,9 @@
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -686,4 +686,4 @@ void CegisUnifEnumDecisionStrategy::registerEvalPtAtSize(Node e,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index e00370f2a..a543bfda0 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -23,7 +23,7 @@
 #include "theory/quantifiers/sygus/cegis.h"
 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -333,6 +333,6 @@ class CegisUnif : public Cegis
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
index 17f2a0c16..2bf8b4611 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp
@@ -24,9 +24,9 @@
 
 #include <numeric>  // for std::iota
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -621,4 +621,4 @@ bool EnumStreamConcrete::increment()
 Node EnumStreamConcrete::getCurrent() { return d_currTerm; }
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h
index c7e4720d2..a72481a38 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.h
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h
@@ -20,7 +20,7 @@
 #include "expr/node.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -299,6 +299,6 @@ class EnumStreamConcrete : public EnumValGenerator
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/sygus/example_eval_cache.cpp b/src/theory/quantifiers/sygus/example_eval_cache.cpp
index 5056fb96d..aea6cb9ef 100644
--- a/src/theory/quantifiers/sygus/example_eval_cache.cpp
+++ b/src/theory/quantifiers/sygus/example_eval_cache.cpp
@@ -17,10 +17,10 @@
 #include "theory/quantifiers/sygus/example_min_eval.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 
-using namespace CVC5;
-using namespace CVC5::kind;
+using namespace cvc5;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -119,4 +119,4 @@ void ExampleEvalCache::clearEvaluationAll() { d_exOutCache.clear(); }
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/example_eval_cache.h b/src/theory/quantifiers/sygus/example_eval_cache.h
index 97ec38ab5..1a70369a5 100644
--- a/src/theory/quantifiers/sygus/example_eval_cache.h
+++ b/src/theory/quantifiers/sygus/example_eval_cache.h
@@ -20,7 +20,7 @@
 #include "expr/node_trie.h"
 #include "theory/quantifiers/sygus/example_infer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -160,6 +160,6 @@ class ExampleEvalCache
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/sygus/example_infer.cpp b/src/theory/quantifiers/sygus/example_infer.cpp
index 12e4f073e..9dc99cab1 100644
--- a/src/theory/quantifiers/sygus/example_infer.cpp
+++ b/src/theory/quantifiers/sygus/example_infer.cpp
@@ -17,10 +17,10 @@
 
 #include "theory/quantifiers/quant_util.h"
 
-using namespace CVC5;
-using namespace CVC5::kind;
+using namespace cvc5;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -275,4 +275,4 @@ bool ExampleInfer::hasExamplesOut(Node f) const
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/example_infer.h b/src/theory/quantifiers/sygus/example_infer.h
index 0e5ee25ac..dd2bf8a0a 100644
--- a/src/theory/quantifiers/sygus/example_infer.h
+++ b/src/theory/quantifiers/sygus/example_infer.h
@@ -21,7 +21,7 @@
 #include "theory/quantifiers/sygus/sygus_unif_io.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -157,6 +157,6 @@ class ExampleInfer
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/sygus/example_min_eval.cpp b/src/theory/quantifiers/sygus/example_min_eval.cpp
index 4cb9bd345..5b3ccec4f 100644
--- a/src/theory/quantifiers/sygus/example_min_eval.cpp
+++ b/src/theory/quantifiers/sygus/example_min_eval.cpp
@@ -18,7 +18,7 @@
 #include "expr/node_algorithm.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -84,4 +84,4 @@ Node EmeEvalTds::eval(TNode n,
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/example_min_eval.h b/src/theory/quantifiers/sygus/example_min_eval.h
index 9af07caba..2105faf2b 100644
--- a/src/theory/quantifiers/sygus/example_min_eval.h
+++ b/src/theory/quantifiers/sygus/example_min_eval.h
@@ -23,7 +23,7 @@
 #include "expr/node.h"
 #include "expr/node_trie.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -118,6 +118,6 @@ class EmeEvalTds : public EmeEval
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.cpp b/src/theory/quantifiers/sygus/rcons_obligation_info.cpp
index 7d4a41f2d..6db446dbb 100644
--- a/src/theory/quantifiers/sygus/rcons_obligation_info.cpp
+++ b/src/theory/quantifiers/sygus/rcons_obligation_info.cpp
@@ -17,7 +17,7 @@
 #include "expr/node_algorithm.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -97,4 +97,4 @@ void RConsObligationInfo::printCandSols(
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.h b/src/theory/quantifiers/sygus/rcons_obligation_info.h
index e05422b59..3bded2a90 100644
--- a/src/theory/quantifiers/sygus/rcons_obligation_info.h
+++ b/src/theory/quantifiers/sygus/rcons_obligation_info.h
@@ -19,7 +19,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -145,6 +145,6 @@ class RConsObligationInfo
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif  // CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
diff --git a/src/theory/quantifiers/sygus/rcons_type_info.cpp b/src/theory/quantifiers/sygus/rcons_type_info.cpp
index 37b136a1c..97ae4878d 100644
--- a/src/theory/quantifiers/sygus/rcons_type_info.cpp
+++ b/src/theory/quantifiers/sygus/rcons_type_info.cpp
@@ -16,7 +16,7 @@
 
 #include "theory/datatypes/sygus_datatype_utils.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -69,4 +69,4 @@ Node RConsTypeInfo::builtinToOb(Node builtin) { return d_ob[builtin]; }
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/rcons_type_info.h b/src/theory/quantifiers/sygus/rcons_type_info.h
index c2bce5720..974897023 100644
--- a/src/theory/quantifiers/sygus/rcons_type_info.h
+++ b/src/theory/quantifiers/sygus/rcons_type_info.h
@@ -19,7 +19,7 @@
 
 #include "theory/quantifiers/sygus/sygus_enumerator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -97,6 +97,6 @@ class RConsTypeInfo
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif  // CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp
index 71853fc76..8df45320f 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp
@@ -29,9 +29,9 @@
 #include "theory/rewriter.h"
 
 using namespace std;
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -187,4 +187,4 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.h b/src/theory/quantifiers/sygus/sygus_abduct.h
index ffcefd38b..634a9a4bd 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.h
+++ b/src/theory/quantifiers/sygus/sygus_abduct.h
@@ -21,7 +21,7 @@
 #include "expr/node.h"
 #include "expr/type_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -85,6 +85,6 @@ class SygusAbduct
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H */
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index c786d2668..82d0c6c62 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -24,9 +24,9 @@
 #include "theory/quantifiers/sygus/type_node_id_trie.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -1214,4 +1214,4 @@ bool SygusEnumerator::TermEnumMasterFv::increment()
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h
index a0d1c9b62..f1ef115f8 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.h
@@ -24,7 +24,7 @@
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -506,6 +506,6 @@ class SygusEnumerator : public EnumValGenerator
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp b/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp
index 51814b07c..e9f41c916 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.cpp
@@ -15,10 +15,10 @@
 
 #include "options/datatypes_options.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -55,4 +55,4 @@ bool EnumValGeneratorBasic::increment()
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h
index c57d6f814..1f489eafc 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h
@@ -25,7 +25,7 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/type_enumerator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -65,6 +65,6 @@ class EnumValGeneratorBasic : public EnumValGenerator
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H */
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
index 3e87ccfc7..5dbd7655f 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -22,10 +22,10 @@
 #include "theory/rewriter.h"
 
 using namespace std;
-using namespace CVC5::kind;
-using namespace CVC5::context;
+using namespace cvc5::kind;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -333,4 +333,4 @@ Node SygusEvalUnfold::unfold(Node en)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h
index d5e47edbc..628f01c40 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h
@@ -21,7 +21,7 @@
 #include "expr/node.h"
 #include "theory/quantifiers/sygus/sygus_invariance.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -154,6 +154,6 @@ class SygusEvalUnfold
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */
diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp
index 26fab8535..95acce626 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.cpp
+++ b/src/theory/quantifiers/sygus/sygus_explain.cpp
@@ -21,10 +21,10 @@
 #include "theory/quantifiers/sygus/sygus_invariance.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -357,4 +357,4 @@ void SygusExplain::getExplanationFor(Node n,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h
index 1b1db568f..477857794 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.h
+++ b/src/theory/quantifiers/sygus/sygus_explain.h
@@ -21,7 +21,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -241,6 +241,6 @@ class SygusExplain
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 554f587c7..1c96b1346 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -30,9 +30,9 @@
 #include "theory/rewriter.h"
 #include "theory/strings/word.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -1622,4 +1622,4 @@ bool CegGrammarConstructor::SygusDatatypeGenerator::shouldInclude(Node op) const
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index a39540452..56f469fef 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -25,7 +25,7 @@
 #include "expr/node.h"
 #include "expr/sygus_datatype.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 /**
@@ -266,6 +266,6 @@ public:
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index fa67e17c4..8a2ad109d 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -31,9 +31,9 @@
 
 #include <numeric>  // for std::iota
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -536,4 +536,4 @@ TypeNode SygusGrammarNorm::normalizeSygusType(TypeNode tn, Node sygus_vars)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index 8c057d2c5..eda34a251 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
@@ -25,7 +25,7 @@
 #include "expr/sygus_datatype.h"
 #include "expr/type_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -426,6 +426,6 @@ class SygusGrammarNorm
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
index 8e6f4fbae..a8ada94ed 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
@@ -22,9 +22,9 @@
 #include "theory/quantifiers/term_util.h"
 
 using namespace std;
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -176,4 +176,4 @@ void SygusRedundantCons::getGenericList(TermDbSygus* tds,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h
index 25256a68c..2144102e0 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h
@@ -22,7 +22,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -118,6 +118,6 @@ class SygusRedundantCons
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index 1c856ffa2..fe286d15c 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -27,7 +27,7 @@
 #include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -358,4 +358,4 @@ bool SygusInterpol::solveInterpolation(const std::string& name,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h
index 34517b6e6..c63d096b8 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.h
+++ b/src/theory/quantifiers/sygus/sygus_interpol.h
@@ -23,7 +23,7 @@
 #include "expr/type_node.h"
 #include "smt/smt_engine.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 /**
@@ -213,6 +213,6 @@ class SygusInterpol
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H */
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp
index 7e6c5ab6c..22ef38b0d 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.cpp
+++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp
@@ -19,10 +19,10 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -261,4 +261,4 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h
index 88e45df45..df2e189e3 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.h
+++ b/src/theory/quantifiers/sygus/sygus_invariance.h
@@ -22,7 +22,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -298,6 +298,6 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */
diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp
index 8dac30c7e..3f2bea9cb 100644
--- a/src/theory/quantifiers/sygus/sygus_module.cpp
+++ b/src/theory/quantifiers/sygus/sygus_module.cpp
@@ -14,7 +14,7 @@
 
 #include "theory/quantifiers/sygus/sygus_module.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -27,4 +27,4 @@ SygusModule::SygusModule(QuantifiersInferenceManager& qim,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index 32f404005..90460eeed 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -21,7 +21,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -157,6 +157,6 @@ class SygusModule
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 25068eb7d..b54b1c940 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -22,10 +22,10 @@
 #include "theory/quantifiers/term_util.h"
 #include "util/random.h"
 
-using namespace CVC5;
-using namespace CVC5::kind;
+using namespace cvc5;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -258,4 +258,4 @@ bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
 
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index c63dcf697..a56a22838 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -19,7 +19,7 @@
 
 #include "theory/quantifiers/sygus/sygus_module.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -168,6 +168,6 @@ class SygusPbe : public SygusModule
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
index dfb0a0f7c..822d19f29 100644
--- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
@@ -22,10 +22,10 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -804,4 +804,4 @@ void SynthConjectureProcess::getComponentVector(Kind k,
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h
index 0b07db89b..6f6e25d0c 100644
--- a/src/theory/quantifiers/sygus/sygus_process_conj.h
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.h
@@ -26,7 +26,7 @@
 #include "expr/node.h"
 #include "expr/type_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -358,6 +358,6 @@ class SynthConjectureProcess
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
index 72ce3f1ab..1b3a52db8 100644
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
@@ -19,9 +19,9 @@
 #include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -144,4 +144,4 @@ Node SygusQePreproc::preprocess(Node q)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
index 49f81df02..26bbf2f92 100644
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
@@ -17,7 +17,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -45,6 +45,6 @@ class SygusQePreproc
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H */
diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
index 723d924f8..55e8c922d 100644
--- a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
@@ -19,9 +19,9 @@
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -488,4 +488,4 @@ void SygusReconstruct::printPool(
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h
index 0512fe643..1f9037a26 100644
--- a/src/theory/quantifiers/sygus/sygus_reconstruct.h
+++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h
@@ -23,7 +23,7 @@
 #include "theory/quantifiers/sygus/rcons_obligation_info.h"
 #include "theory/quantifiers/sygus/rcons_type_info.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -307,6 +307,6 @@ class SygusReconstruct : public expr::NotifyMatch
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif  // CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 2d7dfc4bc..179798222 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -29,9 +29,9 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/smt_engine_subsolver.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -621,4 +621,4 @@ bool SygusRepairConst::getFitToLogicExcludeVar(LogicInfo& logic,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h
index 1e7eeb9fc..b79fa4177 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.h
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.h
@@ -20,7 +20,7 @@
 #include <unordered_set>
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 class LogicInfo;
 
@@ -209,6 +209,6 @@ class SygusRepairConst
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */
diff --git a/src/theory/quantifiers/sygus/sygus_stats.cpp b/src/theory/quantifiers/sygus/sygus_stats.cpp
index da08ec1b5..11dec3e61 100644
--- a/src/theory/quantifiers/sygus/sygus_stats.cpp
+++ b/src/theory/quantifiers/sygus/sygus_stats.cpp
@@ -17,7 +17,7 @@
 
 #include "smt/smt_statistics_registry.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -60,4 +60,4 @@ SygusStatistics::~SygusStatistics()
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_stats.h b/src/theory/quantifiers/sygus/sygus_stats.h
index d89fa0eca..7a8ae8ce9 100644
--- a/src/theory/quantifiers/sygus/sygus_stats.h
+++ b/src/theory/quantifiers/sygus/sygus_stats.h
@@ -19,7 +19,7 @@
 
 #include "util/statistics_registry.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -53,6 +53,6 @@ class SygusStatistics
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp
index 8eb13fef8..2d72b4fab 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif.cpp
@@ -19,9 +19,9 @@
 #include "util/random.h"
 
 using namespace std;
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -136,4 +136,4 @@ void SygusUnif::print_val(const char* c, std::vector<Node>& vals, bool pol)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
index 153c4603b..1ed81194a 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.h
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -21,7 +21,7 @@
 #include "expr/node.h"
 #include "theory/quantifiers/sygus/sygus_unif_strat.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -193,6 +193,6 @@ class SygusUnif
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
index be24cb9e7..9dfac1d68 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp
@@ -26,9 +26,9 @@
 
 #include <math.h>
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -1677,4 +1677,4 @@ Node SygusUnifIo::constructBestConditional(Node ce,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h
index 5d4f7fb7d..825e5741d 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.h
@@ -20,7 +20,7 @@
 #include <map>
 #include "theory/quantifiers/sygus/sygus_unif.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -468,6 +468,6 @@ class SygusUnifIo : public SygusUnif
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 436678aa9..c3cff70d9 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -24,9 +24,9 @@
 
 #include <math.h>
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -1207,4 +1207,4 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::computeCond(Node cond,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index 82f2a80d2..51c49cbef 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -23,7 +23,7 @@
 
 #include "theory/quantifiers/lazy_trie.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -443,6 +443,6 @@ class SygusUnifRl : public SygusUnif
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index 5551be630..24bcb1eab 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -24,9 +24,9 @@
 #include "theory/rewriter.h"
 
 using namespace std;
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -1050,4 +1050,4 @@ void SygusUnifStrategy::indent(const char* c, int ind)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h
index c9d6e5d96..2508fdc9b 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -20,7 +20,7 @@
 #include <map>
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -428,6 +428,6 @@ class SygusUnifStrategy
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */
diff --git a/src/theory/quantifiers/sygus/sygus_utils.cpp b/src/theory/quantifiers/sygus/sygus_utils.cpp
index ec5edd640..6c14aaa80 100644
--- a/src/theory/quantifiers/sygus/sygus_utils.cpp
+++ b/src/theory/quantifiers/sygus/sygus_utils.cpp
@@ -20,9 +20,9 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -179,4 +179,4 @@ TypeNode SygusUtils::getSygusTypeForSynthFun(Node f)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/sygus_utils.h b/src/theory/quantifiers/sygus/sygus_utils.h
index 2646dd1c8..0ec497789 100644
--- a/src/theory/quantifiers/sygus/sygus_utils.h
+++ b/src/theory/quantifiers/sygus/sygus_utils.h
@@ -22,7 +22,7 @@
 #include "expr/node.h"
 #include "expr/subs.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -110,6 +110,6 @@ class SygusUtils
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H */
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 0bfa73048..f7566e7a2 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -37,10 +37,10 @@
 #include "theory/rewriter.h"
 #include "theory/smt_engine_subsolver.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -1353,4 +1353,4 @@ ExampleEvalCache* SynthConjecture::getExampleEvalCache(Node e)
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index e39f65d80..7fd1ae4b3 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -32,7 +32,7 @@
 #include "theory/quantifiers/sygus/sygus_stats.h"
 #include "theory/quantifiers/sygus/template_infer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -426,6 +426,6 @@ class SynthConjecture
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 4f1a0bbbb..3d5406f27 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -20,9 +20,9 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_registry.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -290,4 +290,4 @@ void SynthEngine::preregisterAssertion(Node n)
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index 30f9c181e..a5fde8476 100644
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -24,7 +24,7 @@
 #include "theory/quantifiers/sygus/sygus_stats.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -115,6 +115,6 @@ class SynthEngine : public QuantifiersModule
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/sygus/template_infer.cpp b/src/theory/quantifiers/sygus/template_infer.cpp
index 84fcafd05..875b25370 100644
--- a/src/theory/quantifiers/sygus/template_infer.cpp
+++ b/src/theory/quantifiers/sygus/template_infer.cpp
@@ -19,9 +19,9 @@
 #include "theory/quantifiers/sygus/sygus_utils.h"
 #include "theory/quantifiers/term_util.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -203,4 +203,4 @@ Node SygusTemplateInfer::getTemplateArg(Node prog) const
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/template_infer.h b/src/theory/quantifiers/sygus/template_infer.h
index be35025bd..1ab97b651 100644
--- a/src/theory/quantifiers/sygus/template_infer.h
+++ b/src/theory/quantifiers/sygus/template_infer.h
@@ -22,7 +22,7 @@
 #include "expr/node.h"
 #include "theory/quantifiers/sygus/transition_inference.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -71,6 +71,6 @@ class SygusTemplateInfer
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index f50e222ff..34a81467a 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -30,9 +30,9 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -1091,4 +1091,4 @@ bool TermDbSygus::isEvaluationPoint(Node n) const
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 0bd0c636a..fb7e38ff8 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -28,7 +28,7 @@
 #include "theory/quantifiers/sygus/type_info.h"
 #include "theory/quantifiers/term_database.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -467,6 +467,6 @@ class TermDbSygus {
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */
diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp
index 0b5946176..7ee2f2ec6 100644
--- a/src/theory/quantifiers/sygus/transition_inference.cpp
+++ b/src/theory/quantifiers/sygus/transition_inference.cpp
@@ -20,9 +20,9 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -585,4 +585,4 @@ Node TransitionInference::constructFormulaTrace(DetTrace& dt) const
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/transition_inference.h b/src/theory/quantifiers/sygus/transition_inference.h
index aed003357..8ddc1a320 100644
--- a/src/theory/quantifiers/sygus/transition_inference.h
+++ b/src/theory/quantifiers/sygus/transition_inference.h
@@ -27,7 +27,7 @@
 #include "theory/quantifiers/inst_match_trie.h"
 #include "theory/quantifiers/single_inv_partition.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -332,6 +332,6 @@ class TransitionInference
 
 }  // namespace quantifiers
 }  // namespace theory
-} // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
index 19dff9936..fdc8ca6a3 100644
--- a/src/theory/quantifiers/sygus/type_info.cpp
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -22,9 +22,9 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/sygus/type_node_id_trie.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -488,4 +488,4 @@ bool SygusTypeInfo::isSubclassVarTrivial() const
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/type_info.h b/src/theory/quantifiers/sygus/type_info.h
index cc78fc526..79413a03c 100644
--- a/src/theory/quantifiers/sygus/type_info.h
+++ b/src/theory/quantifiers/sygus/type_info.h
@@ -21,7 +21,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -253,6 +253,6 @@ class SygusTypeInfo
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H */
diff --git a/src/theory/quantifiers/sygus/type_node_id_trie.cpp b/src/theory/quantifiers/sygus/type_node_id_trie.cpp
index 064543af8..a2c7b264d 100644
--- a/src/theory/quantifiers/sygus/type_node_id_trie.cpp
+++ b/src/theory/quantifiers/sygus/type_node_id_trie.cpp
@@ -14,9 +14,9 @@
 
 #include "theory/quantifiers/sygus/type_node_id_trie.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -49,4 +49,4 @@ void TypeNodeIdTrie::assignIds(std::map<Node, unsigned>& assign,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus/type_node_id_trie.h b/src/theory/quantifiers/sygus/type_node_id_trie.h
index a60afda23..6311cbabe 100644
--- a/src/theory/quantifiers/sygus/type_node_id_trie.h
+++ b/src/theory/quantifiers/sygus/type_node_id_trie.h
@@ -22,7 +22,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -48,6 +48,6 @@ class TypeNodeIdTrie
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H */
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 0b1d91684..81dc5cecb 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -28,7 +28,7 @@
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -553,4 +553,4 @@ void SygusInst::addCeLemma(Node q)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h
index 08fc5ccb3..35b66437b 100644
--- a/src/theory/quantifiers/sygus_inst.h
+++ b/src/theory/quantifiers/sygus_inst.h
@@ -24,7 +24,7 @@
 #include "theory/decision_strategy.h"
 #include "theory/quantifiers/quant_module.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 class QuantifiersEngine;
@@ -147,6 +147,6 @@ class SygusInst : public QuantifiersModule
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 2b89c0c7c..5c7797a1a 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -30,7 +30,7 @@
 #include "util/random.h"
 #include "util/sampler.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -845,4 +845,4 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index 65843dc63..7350f4845 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -23,7 +23,7 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_enumeration.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -320,6 +320,6 @@ class SygusSampler : public LazyTrieEvaluator
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index d6d7933cb..64c2fda76 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -28,10 +28,10 @@
 #include "theory/rewriter.h"
 #include "theory/uf/equality_engine.h"
 
-using namespace CVC5::kind;
-using namespace CVC5::context;
+using namespace cvc5::kind;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -1232,4 +1232,4 @@ Node TermDb::getHoTypeMatchPredicate(TypeNode tn)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index d0812d1d1..2077b3d2d 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -28,7 +28,7 @@
 #include "theory/theory.h"
 #include "theory/type_enumerator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -422,6 +422,6 @@ class TermDb : public QuantifiersUtil {
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */
diff --git a/src/theory/quantifiers/term_enumeration.cpp b/src/theory/quantifiers/term_enumeration.cpp
index 2945750c1..a13a19a77 100644
--- a/src/theory/quantifiers/term_enumeration.cpp
+++ b/src/theory/quantifiers/term_enumeration.cpp
@@ -16,9 +16,9 @@
 
 #include "theory/quantifiers/quant_bound_inference.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -75,4 +75,4 @@ bool TermEnumeration::getDomain(TypeNode tn, std::vector<Node>& dom)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h
index fa7eaf63e..bd545ff50 100644
--- a/src/theory/quantifiers/term_enumeration.h
+++ b/src/theory/quantifiers/term_enumeration.h
@@ -24,7 +24,7 @@
 #include "expr/type_node.h"
 #include "theory/type_enumerator.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -71,6 +71,6 @@ class TermEnumeration
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */
diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index cf33f0a41..8317271f9 100644
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -20,7 +20,7 @@
 #include "theory/quantifiers/fmf/first_order_model_fmc.h"
 #include "theory/quantifiers/quantifiers_state.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -134,4 +134,4 @@ bool TermRegistry::useFmcModel() const { return d_useFmcModel; }
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h
index e4e4a7e9f..79070fae8 100644
--- a/src/theory/quantifiers/term_registry.h
+++ b/src/theory/quantifiers/term_registry.h
@@ -25,7 +25,7 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -99,6 +99,6 @@ class TermRegistry
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H */
diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp
index 546f6aa6c..e4e63787e 100644
--- a/src/theory/quantifiers/term_tuple_enumerator.cpp
+++ b/src/theory/quantifiers/term_tuple_enumerator.cpp
@@ -31,7 +31,7 @@
 #include "theory/quantifiers/term_util.h"
 #include "util/statistics_registry.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 template <typename T>
 static CVC4ostream& operator<<(CVC4ostream& out, const std::vector<T>& v)
@@ -505,4 +505,4 @@ TermTupleEnumeratorInterface* mkTermTupleEnumeratorRd(
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/term_tuple_enumerator.h b/src/theory/quantifiers/term_tuple_enumerator.h
index b15ab2212..4d6eb52f8 100644
--- a/src/theory/quantifiers/term_tuple_enumerator.h
+++ b/src/theory/quantifiers/term_tuple_enumerator.h
@@ -18,7 +18,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -94,5 +94,5 @@ TermTupleEnumeratorInterface* mkTermTupleEnumeratorRd(
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 #endif /* TERM_TUPLE_ENUMERATOR_H_7640 */
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 41e06a708..8b1c1aa30 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -22,9 +22,9 @@
 #include "theory/strings/word.h"
 #include "theory/rewriter.h"
 
-using namespace CVC5::kind;
+using namespace cvc5::kind;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -601,4 +601,4 @@ bool TermUtil::hasOffsetArg(Kind ik, int arg, int& offset, Kind& ok)
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 1ac6ca495..d8a881e2e 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -22,7 +22,7 @@
 #include "expr/attribute.h"
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 
 // attribute for "contains instantiation constants from"
@@ -206,6 +206,6 @@ public:
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H */
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index d89abf076..c3c3fe7b6 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -22,10 +22,10 @@
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/valuation.h"
 
-using namespace CVC5::kind;
-using namespace CVC5::context;
+using namespace cvc5::kind;
+using namespace cvc5::context;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -184,4 +184,4 @@ void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::v
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 6af0e8648..21c30390c 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -30,7 +30,7 @@
 #include "theory/theory.h"
 #include "theory/valuation.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -98,6 +98,6 @@ class TheoryQuantifiers : public Theory {
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H */
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index e990f5320..53c077930 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -22,7 +22,7 @@
 #include "expr/node.h"
 #include "expr/type_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
@@ -131,6 +131,6 @@ struct QuantifierInstPatternListTypeRule {
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H */
author	Aina Niemetz <aina.niemetz@gmail.com>	2021-04-01 09:56:14 -0700
committer	GitHub <noreply@github.com>	2021-04-01 16:56:14 +0000
commit	05a53a2ac405bcd18a84024247145f161809c3b0 (patch)
tree	34241c0a82f79d717ddbfbb0c294f9a09c7edb0c /src/theory/quantifiers
parent	afaf4413775ff7d6054a5893f1397ad908e0773c (diff)