Rename namespace CVC5 to cvc5. (#6258)

69 files changed, 207 insertions, 207 deletions

diff --git a/src/prop/README.minisat b/src/prop/README.minisat
index 081e79191..b3e101a88 100644
--- a/src/prop/README.minisat
+++ b/src/prop/README.minisat
@@ -4,7 +4,7 @@ This is MiniSAT 2.2.0, downloaded from here:
 
 on 11 July 2010.
 
-The code has been modified to put everything in the CVC5::MiniSat
+The code has been modified to put everything in the cvc5::MiniSat
 namespace.  The build process has been modified.  Other parts have
 been modified to serve CVC4's purposes.
 
diff --git a/src/prop/bv_sat_solver_notify.h b/src/prop/bv_sat_solver_notify.h
index 1645a096a..fe95e7adb 100644
--- a/src/prop/bv_sat_solver_notify.h
+++ b/src/prop/bv_sat_solver_notify.h
@@ -21,7 +21,7 @@
 #include "prop/sat_solver_types.h"
 #include "util/resource_manager.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 class BVSatSolverNotify {
@@ -45,6 +45,6 @@ public:
 };/* class BVSatSolverInterface::Notify */
 
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index fb764631f..ba1a7fc3b 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -20,7 +20,7 @@
 #include "proof/clause_id.h"
 #include "util/statistics_registry.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name)
@@ -298,4 +298,4 @@ void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
 }
 
 }  // namespace prop
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 2a099ad21..1bc0eb237 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -28,7 +28,7 @@
 #include "util/statistics_registry.h"
 #include "util/stats_timer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 class BVMinisatSatSolver : public BVSatSolverInterface,
@@ -148,4 +148,4 @@ public:
 };
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/bvminisat/core/Dimacs.h b/src/prop/bvminisat/core/Dimacs.h
index be82fb557..a660391f7 100644
--- a/src/prop/bvminisat/core/Dimacs.h
+++ b/src/prop/bvminisat/core/Dimacs.h
@@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/core/SolverTypes.h"
 #include "prop/bvminisat/utils/ParseUtils.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -86,6 +86,6 @@ static void parse_DIMACS(gzFile input_stream, Solver& S) {
 
 //=================================================================================================
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index d7dc3f6d4..d154b5e7f 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -34,7 +34,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "theory/interrupted.h"
 #include "util/utility.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace BVMinisat {
 
 #define OUTPUT_TAG "bvminisat: [a=" << assumptions.size() << ",l=" << decisionLevel() << "] "
@@ -82,7 +82,7 @@ CRef Solver::TCRef_Lazy = CRef_Undef - 1; // no real lazy ref here
 //=================================================================================================
 // Constructor/Destructor:
 
-Solver::Solver(CVC5::context::Context* context)
+Solver::Solver(cvc5::context::Context* context)
     :
 
       // Parameters (user settable):
@@ -976,7 +976,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
         return l_False;
       }
 
-      if (!CVC5::options::bvEagerExplanations())
+      if (!cvc5::options::bvEagerExplanations())
       {
         // check if uip leads to a conflict
         if (backtrack_level < assumptions.size())
@@ -1028,7 +1028,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
         isWithinBudget =
             withinBudget(ResourceManager::Resource::BvSatConflictsStep);
       }
-      catch (const CVC5::theory::Interrupted& e)
+      catch (const cvc5::theory::Interrupted& e)
       {
         // do some clean-up and rethrow
         cancelUntil(assumptions.size());
@@ -1418,4 +1418,4 @@ bool Solver::withinBudget(ResourceManager::Resource r) const
 }
 
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 6386c33fa..3bd43f889 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -33,7 +33,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/utils/Options.h"
 #include "util/resource_manager.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 namespace BVMinisat {
 class Solver;
@@ -80,7 +80,7 @@ private:
     Notify* d_notify;
 
     /** Cvc4 context */
-    CVC5::context::Context* c;
+    cvc5::context::Context* c;
 
     /** True constant */
     Var varTrue;
@@ -92,7 +92,7 @@ public:
 
     // Constructor/Destructor:
     //
- Solver(CVC5::context::Context* c);
+ Solver(cvc5::context::Context* c);
  virtual ~Solver();
 
  void setNotify(Notify* toNotify);
@@ -534,6 +534,6 @@ inline void     Solver::toDimacs     (const char* file, Lit p, Lit q, Lit r){ ve
 
 //=================================================================================================
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/bvminisat/core/SolverTypes.h b/src/prop/bvminisat/core/SolverTypes.h
index 96022efbf..fd0e86116 100644
--- a/src/prop/bvminisat/core/SolverTypes.h
+++ b/src/prop/bvminisat/core/SolverTypes.h
@@ -28,15 +28,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/mtl/Map.h"
 #include "prop/bvminisat/mtl/Vec.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace BVMinisat {
 class Solver;
 }
 template <class Solver>
 class TSatProof;
-}  // namespace CVC5
+}  // namespace cvc5
 
-namespace CVC5 {
+namespace cvc5 {
 
 namespace BVMinisat {
 
@@ -430,6 +430,6 @@ inline void Clause::strengthen(Lit p)
 
 //=================================================================================================
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Alg.h b/src/prop/bvminisat/mtl/Alg.h
index 0b173eb08..ae72ca878 100644
--- a/src/prop/bvminisat/mtl/Alg.h
+++ b/src/prop/bvminisat/mtl/Alg.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "base/check.h"
 #include "prop/bvminisat/mtl/Vec.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -82,6 +82,6 @@ static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true);
 
 //=================================================================================================
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Alloc.h b/src/prop/bvminisat/mtl/Alloc.h
index 582db74f1..2697f13b9 100644
--- a/src/prop/bvminisat/mtl/Alloc.h
+++ b/src/prop/bvminisat/mtl/Alloc.h
@@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/mtl/Vec.h"
 #include "prop/bvminisat/mtl/XAlloc.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -149,6 +149,6 @@ RegionAllocator<T>::alloc(int size)
 
 //=================================================================================================
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Heap.h b/src/prop/bvminisat/mtl/Heap.h
index 7b04a5091..73c1f07d2 100644
--- a/src/prop/bvminisat/mtl/Heap.h
+++ b/src/prop/bvminisat/mtl/Heap.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "base/check.h"
 #include "prop/bvminisat/mtl/Vec.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -156,6 +156,6 @@ class Heap {
 
 //=================================================================================================
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Map.h b/src/prop/bvminisat/mtl/Map.h
index fd64fc751..2d5db2561 100644
--- a/src/prop/bvminisat/mtl/Map.h
+++ b/src/prop/bvminisat/mtl/Map.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/mtl/IntTypes.h"
 #include "prop/bvminisat/mtl/Vec.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -191,6 +191,6 @@ class Map {
 
 //=================================================================================================
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Queue.h b/src/prop/bvminisat/mtl/Queue.h
index a72660337..8407fd7ee 100644
--- a/src/prop/bvminisat/mtl/Queue.h
+++ b/src/prop/bvminisat/mtl/Queue.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "base/check.h"
 #include "prop/bvminisat/mtl/Vec.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -86,6 +86,6 @@ public:
 
 //=================================================================================================
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Sort.h b/src/prop/bvminisat/mtl/Sort.h
index 1cfa220ab..30b3b5396 100644
--- a/src/prop/bvminisat/mtl/Sort.h
+++ b/src/prop/bvminisat/mtl/Sort.h
@@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 //=================================================================================================
 // Some sorting algorithms for vec's
 
-namespace CVC5 {
+namespace cvc5 {
 namespace BVMinisat {
 
 template<class T>
@@ -94,6 +94,6 @@ template <class T> void sort(vec<T>& v) {
 
 //=================================================================================================
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Vec.h b/src/prop/bvminisat/mtl/Vec.h
index c918fc4a0..047a89991 100644
--- a/src/prop/bvminisat/mtl/Vec.h
+++ b/src/prop/bvminisat/mtl/Vec.h
@@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/mtl/IntTypes.h"
 #include "prop/bvminisat/mtl/XAlloc.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -147,6 +147,6 @@ void vec<T>::clear(bool dealloc) {
 
 //=================================================================================================
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/XAlloc.h b/src/prop/bvminisat/mtl/XAlloc.h
index 1500114a2..581915d36 100644
--- a/src/prop/bvminisat/mtl/XAlloc.h
+++ b/src/prop/bvminisat/mtl/XAlloc.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <errno.h>
 #include <stdlib.h>
 
-namespace CVC5 {
+namespace cvc5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -42,6 +42,6 @@ static inline void* xrealloc(void *ptr, size_t size)
 
 //=================================================================================================
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index b4f9bd354..96ab5b526 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/mtl/Sort.h"
 #include "prop/bvminisat/utils/System.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -48,7 +48,7 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of
 //=================================================================================================
 // Constructor/Destructor:
 
-SimpSolver::SimpSolver(CVC5::context::Context* context)
+SimpSolver::SimpSolver(cvc5::context::Context* context)
     : Solver(context),
       grow(opt_grow),
       clause_lim(opt_clause_lim),
@@ -57,9 +57,9 @@ SimpSolver::SimpSolver(CVC5::context::Context* context)
       use_asymm(opt_use_asymm),
       use_rcheck(opt_use_rcheck),
       use_elim(opt_use_elim
-               && CVC5::options::bitblastMode()
-                      == CVC5::options::BitblastMode::EAGER
-               && !CVC5::options::produceModels()),
+               && cvc5::options::bitblastMode()
+                      == cvc5::options::BitblastMode::EAGER
+               && !cvc5::options::produceModels()),
       merges(0),
       asymm_lits(0),
       eliminated_vars(0),
@@ -94,7 +94,7 @@ SimpSolver::SimpSolver(CVC5::context::Context* context)
 
 SimpSolver::~SimpSolver()
 {
-  //  CVC5::StatisticsRegistry::unregisterStat(&total_eliminate_time);
+  //  cvc5::StatisticsRegistry::unregisterStat(&total_eliminate_time);
 }
 
 
@@ -644,7 +644,7 @@ void SimpSolver::extendModel()
 
 bool SimpSolver::eliminate(bool turn_off_elim)
 {
-  //  CVC5::TimerStat::CodeTimer codeTimer(total_eliminate_time);
+  //  cvc5::TimerStat::CodeTimer codeTimer(total_eliminate_time);
 
   if (!simplify())
     return false;
@@ -809,4 +809,4 @@ void SimpSolver::garbageCollect()
 }
 
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h
index 6afdc6ba7..b103243d3 100644
--- a/src/prop/bvminisat/simp/SimpSolver.h
+++ b/src/prop/bvminisat/simp/SimpSolver.h
@@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/core/Solver.h"
 #include "prop/bvminisat/mtl/Queue.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 namespace context {
 class Context;
@@ -41,7 +41,7 @@ class SimpSolver : public Solver {
  public:
     // Constructor/Destructor:
     //
-  SimpSolver(CVC5::context::Context* context);
+  SimpSolver(cvc5::context::Context* context);
   ~SimpSolver();
 
   // Problem specification:
@@ -115,7 +115,7 @@ class SimpSolver : public Solver {
     int     merges;
     int     asymm_lits;
     int     eliminated_vars;
-    //    CVC5::TimerStat total_eliminate_time;
+    //    cvc5::TimerStat total_eliminate_time;
 
    protected:
 
@@ -238,6 +238,6 @@ inline lbool SimpSolver::solveLimited (bool do_simp, bool turn_off_simp){
 
 //=================================================================================================
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/bvminisat/utils/Options.cc b/src/prop/bvminisat/utils/Options.cc
index 44c642441..0b05d5cf6 100644
--- a/src/prop/bvminisat/utils/Options.cc
+++ b/src/prop/bvminisat/utils/Options.cc
@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/mtl/Sort.h"
 #include "prop/bvminisat/utils/ParseUtils.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace BVMinisat {
 
 void BVMinisat::parseOptions(int& argc, char** argv, bool strict)
@@ -91,4 +91,4 @@ void BVMinisat::printUsageAndExit (int argc, char** argv, bool verbose)
 }
 
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/bvminisat/utils/Options.h b/src/prop/bvminisat/utils/Options.h
index e7b6942bd..033ffb64f 100644
--- a/src/prop/bvminisat/utils/Options.h
+++ b/src/prop/bvminisat/utils/Options.h
@@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/mtl/Vec.h"
 #include "prop/bvminisat/utils/ParseUtils.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace BVMinisat {
 
 //==================================================================================================
@@ -432,6 +432,6 @@ class BoolOption : public Option
 
 //=================================================================================================
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/bvminisat/utils/ParseUtils.h b/src/prop/bvminisat/utils/ParseUtils.h
index a748651db..d69856ebb 100644
--- a/src/prop/bvminisat/utils/ParseUtils.h
+++ b/src/prop/bvminisat/utils/ParseUtils.h
@@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 //#include <zlib.h>
 #include <unistd.h>
 
-namespace CVC5 {
+namespace cvc5 {
 namespace BVMinisat {
 
 //-------------------------------------------------------------------------------------------------
@@ -120,6 +120,6 @@ static bool eagerMatch(B& in, const char* str) {
 
 //=================================================================================================
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/bvminisat/utils/System.cc b/src/prop/bvminisat/utils/System.cc
index 9b9f99eb5..606fc5cbe 100644
--- a/src/prop/bvminisat/utils/System.cc
+++ b/src/prop/bvminisat/utils/System.cc
@@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <stdio.h>
 #include <stdlib.h>
 
-namespace CVC5 {
+namespace cvc5 {
 namespace BVMinisat {
 
 // TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and
@@ -95,5 +95,5 @@ double BVMinisat::memUsed() {
     return 0; }
 #endif
 
-} /* CVC5::BVMinisat namespace */
+} /* cvc5::BVMinisat namespace */
 } /* CVC4 namespace */
diff --git a/src/prop/bvminisat/utils/System.h b/src/prop/bvminisat/utils/System.h
index 117fbfa3d..c805c232a 100644
--- a/src/prop/bvminisat/utils/System.h
+++ b/src/prop/bvminisat/utils/System.h
@@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 //-------------------------------------------------------------------------------------------------
 
-namespace CVC5 {
+namespace cvc5 {
 namespace BVMinisat {
 
 static inline double cpuTime(void); // CPU-time in seconds.
@@ -37,7 +37,7 @@ extern double memUsed();            // Memory in mega bytes (returns 0 for unsup
 extern double memUsedPeak();        // Peak-memory in mega bytes (returns 0 for unsupported architectures).
 
 }  // namespace BVMinisat
-}  // namespace CVC5
+}  // namespace cvc5
 
 //-------------------------------------------------------------------------------------------------
 // Implementation of inline functions:
@@ -45,7 +45,7 @@ extern double memUsedPeak();        // Peak-memory in mega bytes (returns 0 for
 #if defined(_MSC_VER) || defined(__MINGW32__)
 #include <time.h>
 
-static inline double CVC5::BVMinisat::cpuTime(void)
+static inline double cvc5::BVMinisat::cpuTime(void)
 {
   return (double)clock() / CLOCKS_PER_SEC;
 }
@@ -55,7 +55,7 @@ static inline double CVC5::BVMinisat::cpuTime(void)
 #include <sys/resource.h>
 #include <unistd.h>
 
-static inline double CVC5::BVMinisat::cpuTime(void)
+static inline double cvc5::BVMinisat::cpuTime(void)
 {
   struct rusage ru;
   getrusage(RUSAGE_SELF, &ru);
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index 9bad7072a..cac015904 100644
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -20,7 +20,7 @@
 
 #include "base/check.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 using CadicalLit = int;
@@ -200,6 +200,6 @@ CadicalSolver::Statistics::~Statistics() {
 }
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif  // CVC4_USE_CADICAL
diff --git a/src/prop/cadical.h b/src/prop/cadical.h
index c49aa8d03..910e5def5 100644
--- a/src/prop/cadical.h
+++ b/src/prop/cadical.h
@@ -26,7 +26,7 @@
 
 #include <cadical.hpp>
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 class CadicalSolver : public SatSolver
@@ -103,7 +103,7 @@ class CadicalSolver : public SatSolver
 };
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif  // CVC4_USE_CADICAL
 #endif  // CVC4__PROP__CADICAL_H
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index bd23bad94..1caea7bb7 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -37,7 +37,7 @@
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 CnfStream::CnfStream(SatSolver* satSolver,
@@ -788,4 +788,4 @@ void CnfStream::convertAndAssert(TNode node, bool negated)
 }
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index af86da746..b39423d71 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -34,7 +34,7 @@
 #include "prop/registrar.h"
 #include "prop/sat_solver_types.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 class OutputManager;
 
@@ -318,6 +318,6 @@ class CnfStream {
 }; /* class CnfStream */
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__PROP__CNF_STREAM_H */
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index 91fc12c6c..ce5e4e2b0 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -22,7 +22,7 @@
 
 #include <cryptominisat5/cryptominisat.h>
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 using CMSatVar = unsigned;
@@ -244,5 +244,5 @@ CryptoMinisatSolver::Statistics::~Statistics() {
 }
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
 #endif
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index fb118619c..65e1196f3 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -33,7 +33,7 @@ namespace CMSat {
   class SATSolver;
 }
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 class CryptoMinisatSolver : public SatSolver
@@ -106,7 +106,7 @@ class CryptoMinisatSolver : public SatSolver
 };
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif  // CVC4_USE_CRYPTOMINISAT
 #endif  // CVC4__PROP__CRYPTOMINISAT_H
diff --git a/src/prop/kissat.cpp b/src/prop/kissat.cpp
index ccca3a3b4..10b7b07de 100644
--- a/src/prop/kissat.cpp
+++ b/src/prop/kissat.cpp
@@ -20,7 +20,7 @@
 
 #include "base/check.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 using KissatLit = int32_t;
@@ -173,6 +173,6 @@ KissatSolver::Statistics::~Statistics()
 }
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif  // CVC4_USE_KISSAT
diff --git a/src/prop/kissat.h b/src/prop/kissat.h
index 7bfcbac68..6984a7e50 100644
--- a/src/prop/kissat.h
+++ b/src/prop/kissat.h
@@ -28,7 +28,7 @@ extern "C" {
 #include <kissat/kissat.h>
 }
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 class KissatSolver : public SatSolver
@@ -97,7 +97,7 @@ class KissatSolver : public SatSolver
 };
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif  // CVC4_USE_KISSAT
 #endif  // CVC4__PROP__KISSAT_H
diff --git a/src/prop/minisat/core/Dimacs.h b/src/prop/minisat/core/Dimacs.h
index b48044457..02182fde3 100644
--- a/src/prop/minisat/core/Dimacs.h
+++ b/src/prop/minisat/core/Dimacs.h
@@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/utils/ParseUtils.h"
 #include "prop/minisat/core/SolverTypes.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -86,6 +86,6 @@ static void parse_DIMACS(gzFile input_stream, Solver& S) {
 
 //=================================================================================================
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 9dbcada15..cd3ae5edf 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -39,9 +39,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/mtl/Sort.h"
 #include "prop/theory_proxy.h"
 
-using namespace CVC5::prop;
+using namespace cvc5::prop;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace Minisat {
 
 namespace {
@@ -83,7 +83,7 @@ static inline void dtviewPropagationHeaderHelper(size_t level)
 // Writes to Trace macro for propagation tracing
 static inline void dtviewBoolPropagationHelper(size_t level,
                                                Lit& l,
-                                               CVC5::prop::TheoryProxy* proxy)
+                                               cvc5::prop::TheoryProxy* proxy)
 {
   Trace("dtview::prop") << std::string(
       level + 1 - (options::incrementalSolving() ? 1 : 0), ' ')
@@ -95,7 +95,7 @@ static inline void dtviewBoolPropagationHelper(size_t level,
 // Writes to Trace macro for conflict tracing
 static inline void dtviewPropConflictHelper(size_t level,
                                             Clause& confl,
-                                            CVC5::prop::TheoryProxy* proxy)
+                                            cvc5::prop::TheoryProxy* proxy)
 {
   Trace("dtview::conflict")
       << std::string(level + 1 - (options::incrementalSolving() ? 1 : 0), ' ')
@@ -148,9 +148,9 @@ class ScopedBool
 //=================================================================================================
 // Constructor/Destructor:
 
-Solver::Solver(CVC5::prop::TheoryProxy* proxy,
-               CVC5::context::Context* context,
-               CVC5::context::UserContext* userContext,
+Solver::Solver(cvc5::prop::TheoryProxy* proxy,
+               cvc5::context::Context* context,
+               cvc5::context::UserContext* userContext,
                ProofNodeManager* pnm,
                bool enableIncremental)
     : d_proxy(proxy),
@@ -548,7 +548,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
                 ProofManager::getCnfProof()->registerConvertedClause(id);
               }
               ProofManager::getSatProof()->finalizeProof(
-                  CVC5::Minisat::CRef_Lazy);
+                  cvc5::Minisat::CRef_Lazy);
             }
             if (isProofEnabled())
             {
@@ -648,7 +648,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
                 id = ProofManager::getSatProof()->storeUnitConflict(
                     ca[confl][0], LEARNT);
                 ProofManager::getSatProof()->finalizeProof(
-                    CVC5::Minisat::CRef_Lazy);
+                    cvc5::Minisat::CRef_Lazy);
               }
               else
               {
@@ -1030,7 +1030,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
           Trace("pf::sat") << "\n";
         }
 
-        Trace("pf::sat") << CVC5::push;
+        Trace("pf::sat") << cvc5::push;
         for (int j = (p == lit_Undef) ? 0 : 1, size = ca[confl].size();
              j < size;
              j++)
@@ -1073,7 +1073,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
             }
           }
         }
-        Trace("pf::sat") << CVC5::pop;
+        Trace("pf::sat") << cvc5::pop;
 
         // Select next clause to look at:
         while (!seen[var(trail[index--])]);
@@ -1326,7 +1326,7 @@ CRef Solver::propagate(TheoryCheckType type)
     // theory propagation
     if (type == CHECK_FINAL) {
       // Do the theory check
-      theoryCheck(CVC5::theory::Theory::EFFORT_FULL);
+      theoryCheck(cvc5::theory::Theory::EFFORT_FULL);
       // Pick up the theory propagated literals (there could be some,
       // if new lemmas are added)
       propagateTheory();
@@ -1350,9 +1350,9 @@ CRef Solver::propagate(TheoryCheckType type)
         if (confl == CRef_Undef && type != CHECK_WITHOUT_THEORY) {
             // Do the theory check
             if (type == CHECK_FINAL_FAKE) {
-              theoryCheck(CVC5::theory::Theory::EFFORT_FULL);
+              theoryCheck(cvc5::theory::Theory::EFFORT_FULL);
             } else {
-              theoryCheck(CVC5::theory::Theory::EFFORT_STANDARD);
+              theoryCheck(cvc5::theory::Theory::EFFORT_STANDARD);
             }
             // Pick up the theory propagated literals
             propagateTheory();
@@ -1439,7 +1439,7 @@ void Solver::propagateTheory() {
 |
 |    Note: the propagation queue might be NOT empty
 |________________________________________________________________________________________________@*/
-void Solver::theoryCheck(CVC5::theory::Theory::Effort effort)
+void Solver::theoryCheck(cvc5::theory::Theory::Effort effort)
 {
   d_proxy->theoryCheck(effort);
 }
@@ -2145,7 +2145,7 @@ void Solver::pop()
   --assertionLevel;
   Debug("minisat") << "in user pop, decreasing assertion level to "
                    << assertionLevel << "\n"
-                   << CVC5::push;
+                   << cvc5::push;
   while (true) {
     Debug("minisat") << "== unassigning " << trail.last() << std::endl;
     Var      x  = var(trail.last());
@@ -2167,7 +2167,7 @@ void Solver::pop()
   // Remove the clauses
   removeClausesAboveLevel(clauses_persistent, assertionLevel);
   removeClausesAboveLevel(clauses_removable, assertionLevel);
-  Debug("minisat") << CVC5::pop;
+  Debug("minisat") << cvc5::pop;
   // Pop the SAT context to notify everyone
   d_context->pop();  // SAT context for CVC4
 
@@ -2347,7 +2347,7 @@ CRef Solver::updateLemmas() {
 
 void ClauseAllocator::reloc(CRef& cr,
                             ClauseAllocator& to,
-                            CVC5::TSatProof<Solver>* proof)
+                            cvc5::TSatProof<Solver>* proof)
 {
   Debug("minisat") << "ClauseAllocator::reloc: cr " << cr << std::endl;
   // FIXME what is this CRef_lazy
@@ -2398,4 +2398,4 @@ std::shared_ptr<ProofNode> Solver::getProof()
 bool Solver::isProofEnabled() const { return d_pfManager != nullptr; }
 
 }  // namespace Minisat
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 53f7a828c..9da0e2f89 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -38,16 +38,16 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "theory/theory.h"
 #include "util/resource_manager.h"
 
-namespace CVC5 {
+namespace cvc5 {
 template <class Solver> class TSatProof;
 
 namespace prop {
 class PropEngine;
 class TheoryProxy;
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
 
-namespace CVC5 {
+namespace cvc5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -56,10 +56,10 @@ namespace Minisat {
 class Solver {
 
   /** The only two CVC4 entry points to the private solver data */
-  friend class CVC5::prop::PropEngine;
-  friend class CVC5::prop::TheoryProxy;
-  friend class CVC5::prop::SatProofManager;
-  friend class CVC5::TSatProof<Minisat::Solver>;
+  friend class cvc5::prop::PropEngine;
+  friend class cvc5::prop::TheoryProxy;
+  friend class cvc5::prop::SatProofManager;
+  friend class cvc5::TSatProof<Minisat::Solver>;
 
  public:
   static CRef TCRef_Undef;
@@ -73,10 +73,10 @@ class Solver {
 
  protected:
   /** The pointer to the proxy that provides interfaces to the SMT engine */
-  CVC5::prop::TheoryProxy* d_proxy;
+  cvc5::prop::TheoryProxy* d_proxy;
 
   /** The context from the SMT solver */
-  CVC5::context::Context* d_context;
+  cvc5::context::Context* d_context;
 
   /** The current assertion level (user) */
   int assertionLevel;
@@ -88,7 +88,7 @@ class Solver {
   Var varFalse;
 
   /** The resolution proof manager */
-  std::unique_ptr<CVC5::prop::SatProofManager> d_pfManager;
+  std::unique_ptr<cvc5::prop::SatProofManager> d_pfManager;
 
  public:
   /** Returns the current user assertion level */
@@ -105,7 +105,7 @@ class Solver {
   vec<bool> lemmas_removable;
 
   /** Nodes being converted to CNF */
-  std::vector<CVC5::Node> lemmas_cnf_assertion;
+  std::vector<cvc5::Node> lemmas_cnf_assertion;
 
   /** Do a another check if FULL_EFFORT was the last one */
   bool recheck;
@@ -134,9 +134,9 @@ public:
 
     // Constructor/Destructor:
     //
- Solver(CVC5::prop::TheoryProxy* proxy,
-        CVC5::context::Context* context,
-        CVC5::context::UserContext* userContext,
+ Solver(cvc5::prop::TheoryProxy* proxy,
+        cvc5::context::Context* context,
+        cvc5::context::UserContext* userContext,
         ProofNodeManager* pnm,
         bool enableIncremental = false);
  virtual ~Solver();
@@ -153,7 +153,7 @@ public:
  Var falseVar() const { return varFalse; }
 
  /** Retrive the SAT proof manager */
- CVC5::prop::SatProofManager* getProofManager();
+ cvc5::prop::SatProofManager* getProofManager();
 
  /** Retrive the refutation proof */
  std::shared_ptr<ProofNode> getProof();
@@ -438,7 +438,7 @@ protected:
     CRef     propagateBool    ();                                                      // Perform Boolean propagation. Returns possibly conflicting clause.
     void     propagateTheory  ();                                                      // Perform Theory propagation.
     void theoryCheck(
-        CVC5::theory::Theory::Effort
+        cvc5::theory::Theory::Effort
             effort);  // Perform a theory satisfiability check. Adds lemmas.
     CRef     updateLemmas     ();                                                      // Add the lemmas, backtraking if necessary and return a conflict if there is one
     void     cancelUntil      (int level);                                             // Backtrack until a certain level.
@@ -666,6 +666,6 @@ inline void     Solver::toDimacs     (const char* file, Lit p, Lit q, Lit r){ ve
 
 //=================================================================================================
 }  // namespace Minisat
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index 4d9dd682d..c3f4279cb 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -31,15 +31,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/mtl/Map.h"
 #include "prop/minisat/mtl/Vec.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace Minisat {
 class Solver;
 }
 template <class Solver>
 class TSatProof;
-}  // namespace CVC5
+}  // namespace cvc5
 
-namespace CVC5 {
+namespace cvc5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -183,9 +183,9 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) {
 }
 
 }  // namespace Minisat
-} // namespace CVC5
+}  // namespace cvc5
 
-namespace CVC5 {
+namespace cvc5 {
 namespace Minisat{
 
 //=================================================================================================
@@ -322,7 +322,7 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
 
     void reloc(CRef& cr,
                ClauseAllocator& to,
-               CVC5::TSatProof<Solver>* proof = NULL);
+               cvc5::TSatProof<Solver>* proof = NULL);
     // Implementation moved to Solver.cc.
 };
 
@@ -500,6 +500,6 @@ inline void Clause::strengthen(Lit p)
 
 //=================================================================================================
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index e95677d57..07b345eda 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -25,7 +25,7 @@
 #include "proof/sat_proof.h"
 #include "util/statistics_registry.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 //// DPllMinisatSatSolver
@@ -301,20 +301,20 @@ void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){
 }
 
 }  // namespace prop
-} // namespace CVC5
+}  // namespace cvc5
 
-namespace CVC5 {
+namespace cvc5 {
 template <>
-prop::SatLiteral toSatLiteral<CVC5::Minisat::Solver>(Minisat::Solver::TLit lit)
+prop::SatLiteral toSatLiteral<cvc5::Minisat::Solver>(Minisat::Solver::TLit lit)
 {
   return prop::MinisatSatSolver::toSatLiteral(lit);
 }
 
 template <>
-void toSatClause<CVC5::Minisat::Solver>(
-    const CVC5::Minisat::Solver::TClause& minisat_cl, prop::SatClause& sat_cl)
+void toSatClause<cvc5::Minisat::Solver>(
+    const cvc5::Minisat::Solver::TClause& minisat_cl, prop::SatClause& sat_cl)
 {
   prop::MinisatSatSolver::toSatClause(minisat_cl, sat_cl);
 }
 
-} // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 7dfeb6aa2..0a36b6297 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -20,7 +20,7 @@
 #include "prop/minisat/simp/SimpSolver.h"
 #include "util/statistics_registry.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 class MinisatSatSolver : public CDCLTSatSolverInterface
@@ -40,7 +40,7 @@ class MinisatSatSolver : public CDCLTSatSolverInterface
   static void  toSatClause    (const Minisat::Clause& clause, SatClause& sat_clause);
   void initialize(context::Context* context,
                   TheoryProxy* theoryProxy,
-                  CVC5::context::UserContext* userContext,
+                  cvc5::context::UserContext* userContext,
                   ProofNodeManager* pnm) override;
 
   ClauseId addClause(SatClause& clause, bool removable) override;
@@ -119,4 +119,4 @@ class MinisatSatSolver : public CDCLTSatSolverInterface
 }; /* class MinisatSatSolver */
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h
index 37bc4b7b6..69b782da9 100644
--- a/src/prop/minisat/mtl/Alg.h
+++ b/src/prop/minisat/mtl/Alg.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "base/check.h"
 #include "prop/minisat/mtl/Vec.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -82,6 +82,6 @@ static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true);
 
 //=================================================================================================
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/minisat/mtl/Alloc.h b/src/prop/minisat/mtl/Alloc.h
index 850aaeb73..f6e6d64b2 100644
--- a/src/prop/minisat/mtl/Alloc.h
+++ b/src/prop/minisat/mtl/Alloc.h
@@ -25,7 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/mtl/Vec.h"
 #include "prop/minisat/mtl/XAlloc.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -149,6 +149,6 @@ RegionAllocator<T>::alloc(int size)
 
 //=================================================================================================
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h
index e2ad1513f..7a88c874d 100644
--- a/src/prop/minisat/mtl/Heap.h
+++ b/src/prop/minisat/mtl/Heap.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "base/check.h"
 #include "prop/minisat/mtl/Vec.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -156,6 +156,6 @@ class Heap {
 
 //=================================================================================================
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h
index 2efed4433..1c48f3962 100644
--- a/src/prop/minisat/mtl/Map.h
+++ b/src/prop/minisat/mtl/Map.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/mtl/IntTypes.h"
 #include "prop/minisat/mtl/Vec.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -191,6 +191,6 @@ class Map {
 
 //=================================================================================================
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h
index ef30591bf..cdbc22600 100644
--- a/src/prop/minisat/mtl/Queue.h
+++ b/src/prop/minisat/mtl/Queue.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "base/check.h"
 #include "prop/minisat/mtl/Vec.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -86,6 +86,6 @@ public:
 
 //=================================================================================================
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h
index 7cf393847..2b9550d48 100644
--- a/src/prop/minisat/mtl/Sort.h
+++ b/src/prop/minisat/mtl/Sort.h
@@ -26,7 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 //=================================================================================================
 // Some sorting algorithms for vec's
 
-namespace CVC5 {
+namespace cvc5 {
 namespace Minisat {
 
 template<class T>
@@ -94,6 +94,6 @@ template <class T> void sort(vec<T>& v) {
 
 //=================================================================================================
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h
index e17e320d2..5410981f9 100644
--- a/src/prop/minisat/mtl/Vec.h
+++ b/src/prop/minisat/mtl/Vec.h
@@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/mtl/IntTypes.h"
 #include "prop/minisat/mtl/XAlloc.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -147,6 +147,6 @@ void vec<T>::clear(bool dealloc) {
 
 //=================================================================================================
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/minisat/mtl/XAlloc.h b/src/prop/minisat/mtl/XAlloc.h
index 6bd8c02e8..300dbb16b 100644
--- a/src/prop/minisat/mtl/XAlloc.h
+++ b/src/prop/minisat/mtl/XAlloc.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include <errno.h>
 #include <stdlib.h>
 
-namespace CVC5 {
+namespace cvc5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -42,6 +42,6 @@ static inline void* xrealloc(void *ptr, size_t size)
 
 //=================================================================================================
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 52162776b..e29c1032a 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -27,8 +27,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/mtl/Sort.h"
 #include "prop/minisat/utils/System.h"
 
-using namespace CVC5;
-using namespace CVC5::Minisat;
+using namespace cvc5;
+using namespace cvc5::Minisat;
 
 //=================================================================================================
 // Options:
@@ -48,9 +48,9 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of
 //=================================================================================================
 // Constructor/Destructor:
 
-SimpSolver::SimpSolver(CVC5::prop::TheoryProxy* proxy,
-                       CVC5::context::Context* context,
-                       CVC5::context::UserContext* userContext,
+SimpSolver::SimpSolver(cvc5::prop::TheoryProxy* proxy,
+                       cvc5::context::Context* context,
+                       cvc5::context::UserContext* userContext,
                        ProofNodeManager* pnm,
                        bool enableIncremental)
     : Solver(proxy, context, userContext, pnm, enableIncremental),
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 6c8a87d5e..63a5a93fd 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -27,13 +27,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/core/Solver.h"
 #include "prop/minisat/mtl/Queue.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
   class TheoryProxy;
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
-namespace CVC5 {
+namespace cvc5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -42,9 +42,9 @@ class SimpSolver : public Solver {
  public:
     // Constructor/Destructor:
     //
-  SimpSolver(CVC5::prop::TheoryProxy* proxy,
-             CVC5::context::Context* context,
-             CVC5::context::UserContext* userContext,
+  SimpSolver(cvc5::prop::TheoryProxy* proxy,
+             cvc5::context::Context* context,
+             cvc5::context::UserContext* userContext,
              ProofNodeManager* pnm,
              bool enableIncremental = false);
   ~SimpSolver();
@@ -271,6 +271,6 @@ inline lbool SimpSolver::solve        (Lit p, Lit q, Lit r, bool do_simp, bool t
 
  //=================================================================================================
  }  // namespace Minisat
- }  // namespace CVC5
+ }  // namespace cvc5
 
 #endif
diff --git a/src/prop/minisat/utils/Options.h b/src/prop/minisat/utils/Options.h
index f37b6305e..22e4cd6ee 100644
--- a/src/prop/minisat/utils/Options.h
+++ b/src/prop/minisat/utils/Options.h
@@ -29,7 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/mtl/Vec.h"
 #include "prop/minisat/utils/ParseUtils.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace Minisat {
 
 //==================================================================================================
@@ -432,6 +432,6 @@ class BoolOption : public Option
 
 //=================================================================================================
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/minisat/utils/ParseUtils.h b/src/prop/minisat/utils/ParseUtils.h
index 27e454d00..ae8783e96 100644
--- a/src/prop/minisat/utils/ParseUtils.h
+++ b/src/prop/minisat/utils/ParseUtils.h
@@ -27,7 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 //#include <zlib.h>
 #include <unistd.h>
 
-namespace CVC5 {
+namespace cvc5 {
 namespace Minisat {
 
 //-------------------------------------------------------------------------------------------------
@@ -120,6 +120,6 @@ static bool eagerMatch(B& in, const char* str) {
 
 //=================================================================================================
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index ab5c59dd1..76421db9b 100644
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -18,7 +18,7 @@
 #include "prop/minisat/minisat.h"
 #include "theory/builtin/proof_checker.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 ProofCnfStream::ProofCnfStream(context::UserContext* u,
@@ -1012,4 +1012,4 @@ SatLiteral ProofCnfStream::handleIte(TNode node)
 }
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h
index 7c97a2e8e..fcca2cb34 100644
--- a/src/prop/proof_cnf_stream.h
+++ b/src/prop/proof_cnf_stream.h
@@ -27,7 +27,7 @@
 #include "theory/eager_proof_generator.h"
 #include "theory/theory_proof_step_buffer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 class SatProofManager;
@@ -170,6 +170,6 @@ class ProofCnfStream : public ProofGenerator
 };
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/proof_post_processor.cpp b/src/prop/proof_post_processor.cpp
index 7f075ab37..6b31e6053 100644
--- a/src/prop/proof_post_processor.cpp
+++ b/src/prop/proof_post_processor.cpp
@@ -17,7 +17,7 @@
 
 #include "theory/builtin/proof_checker.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 ProofPostprocessCallback::ProofPostprocessCallback(
@@ -105,4 +105,4 @@ void ProofPostproccess::process(std::shared_ptr<ProofNode> pf)
 }
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/proof_post_processor.h b/src/prop/proof_post_processor.h
index c74cb540f..363970117 100644
--- a/src/prop/proof_post_processor.h
+++ b/src/prop/proof_post_processor.h
@@ -23,7 +23,7 @@
 #include "expr/proof_node_updater.h"
 #include "prop/proof_cnf_stream.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 namespace prop {
 
@@ -107,6 +107,6 @@ class ProofPostproccess
 };
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 9032dbb75..efe599106 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -42,7 +42,7 @@
 #include "util/resource_manager.h"
 #include "util/result.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 /** Keeps a boolean flag scoped */
@@ -616,4 +616,4 @@ std::shared_ptr<ProofNode> PropEngine::getProof()
 bool PropEngine::isProofEnabled() const { return d_pfCnfStream != nullptr; }
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 1145961a1..a01668913 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -27,7 +27,7 @@
 #include "theory/trust_node.h"
 #include "util/result.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 class ResourceManager;
 class DecisionEngine;
@@ -381,6 +381,6 @@ class PropEngine
 };
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__PROP_ENGINE_H */
diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp
index cb380f92d..08c13fe5f 100644
--- a/src/prop/prop_proof_manager.cpp
+++ b/src/prop/prop_proof_manager.cpp
@@ -19,7 +19,7 @@
 #include "prop/prop_proof_manager.h"
 #include "prop/sat_solver.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 PropPfManager::PropPfManager(context::UserContext* userContext,
@@ -109,4 +109,4 @@ std::shared_ptr<ProofNode> PropPfManager::getProof()
 }
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h
index d8732c11a..9a080edc1 100644
--- a/src/prop/prop_proof_manager.h
+++ b/src/prop/prop_proof_manager.h
@@ -23,7 +23,7 @@
 #include "prop/proof_post_processor.h"
 #include "prop/sat_proof_manager.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 namespace prop {
 
@@ -92,6 +92,6 @@ class PropPfManager
 }; /* class PropPfManager */
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__PROP__PROOF_MANAGER_H */
diff --git a/src/prop/registrar.h b/src/prop/registrar.h
index d0fc0fe25..ae085b573 100644
--- a/src/prop/registrar.h
+++ b/src/prop/registrar.h
@@ -23,7 +23,7 @@
 #ifndef CVC4__PROP__REGISTRAR_H
 #define CVC4__PROP__REGISTRAR_H
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 class Registrar {
@@ -40,6 +40,6 @@ public:
 };/* class NullRegistrar */
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__PROP__REGISTRAR_H */
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index a11eeaa8a..da9354c2f 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -20,7 +20,7 @@
 #include "prop/minisat/minisat.h"
 #include "theory/theory_proof_step_buffer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 SatProofManager::SatProofManager(Minisat::Solver* solver,
@@ -753,4 +753,4 @@ void SatProofManager::registerSatAssumptions(const std::vector<Node>& assumps)
 }
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h
index 514f0153b..4d45ce3b7 100644
--- a/src/prop/sat_proof_manager.h
+++ b/src/prop/sat_proof_manager.h
@@ -28,7 +28,7 @@ namespace Minisat {
 class Solver;
 }
 
-namespace CVC5 {
+namespace cvc5 {
 
 class ProofNodeManager;
 
@@ -587,6 +587,6 @@ class SatProofManager
 }; /* class SatProofManager */
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__SAT_PROOF_MANAGER_H */
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index f06171775..1f59a7bd6 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -30,7 +30,7 @@
 #include "prop/sat_solver_types.h"
 #include "util/statistics_registry.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 namespace prop {
 
@@ -150,7 +150,7 @@ class CDCLTSatSolverInterface : public SatSolver
 
   virtual void initialize(context::Context* context,
                           prop::TheoryProxy* theoryProxy,
-                          CVC5::context::UserContext* userContext,
+                          cvc5::context::UserContext* userContext,
                           ProofNodeManager* pnm) = 0;
 
   virtual void push() = 0;
@@ -209,6 +209,6 @@ inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) {
 }
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__PROP__SAT_MODULE_H */
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index 1d933dce8..117210431 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -22,7 +22,7 @@
 #include "prop/kissat.h"
 #include "prop/minisat/minisat.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 BVSatSolverInterface* SatSolverFactory::createMinisat(
@@ -76,4 +76,4 @@ SatSolver* SatSolverFactory::createKissat(StatisticsRegistry* registry,
 }
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index 97b018e09..71e28ac39 100644
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -27,7 +27,7 @@
 #include "prop/sat_solver.h"
 #include "util/statistics_registry.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 class SatSolverFactory
@@ -50,6 +50,6 @@ class SatSolverFactory
 }; /* class SatSolverFactory */
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif  // CVC4__PROP__SAT_SOLVER_FACTORY_H
diff --git a/src/prop/sat_solver_types.cpp b/src/prop/sat_solver_types.cpp
index 3380329c3..13494221e 100644
--- a/src/prop/sat_solver_types.cpp
+++ b/src/prop/sat_solver_types.cpp
@@ -18,11 +18,11 @@
 
 #include <algorithm>
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 bool SatClauseLessThan::operator()(const SatClause& l, const SatClause& r) const
 {
   return std::lexicographical_compare(l.begin(), l.end(), r.begin(), r.end());
 }
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h
index 392dfb2b1..0ab0cba53 100644
--- a/src/prop/sat_solver_types.h
+++ b/src/prop/sat_solver_types.h
@@ -29,7 +29,7 @@
 #include <unordered_set>
 #include <vector>
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 /**
@@ -235,4 +235,4 @@ enum SatSolverLifespan
 };
 
 }
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp
index a0819e571..dbc640d8c 100644
--- a/src/prop/skolem_def_manager.cpp
+++ b/src/prop/skolem_def_manager.cpp
@@ -16,7 +16,7 @@
 
 #include "expr/attribute.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 SkolemDefManager::SkolemDefManager(context::Context* context,
@@ -170,4 +170,4 @@ void SkolemDefManager::getSkolems(
 }
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/skolem_def_manager.h b/src/prop/skolem_def_manager.h
index 6f4ec031f..11b726c2a 100644
--- a/src/prop/skolem_def_manager.h
+++ b/src/prop/skolem_def_manager.h
@@ -26,7 +26,7 @@
 #include "context/context.h"
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 /**
@@ -86,6 +86,6 @@ class SkolemDefManager
 };
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__PROP__SKOLEM_DEF_MANAGER_H */
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index ffec0c365..4a95591b4 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -28,7 +28,7 @@
 #include "theory/theory_engine.h"
 #include "util/statistics_registry.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 
 TheoryProxy::TheoryProxy(PropEngine* propEngine,
@@ -105,7 +105,7 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
 
   theory::TrustNode tte = d_theoryEngine->getExplanation(lNode);
   Node theoryExplanation = tte.getNode();
-  if (CVC5::options::produceProofs())
+  if (cvc5::options::produceProofs())
   {
     d_propEngine->getProofCnfStream()->convertPropagation(tte);
   }
@@ -233,4 +233,4 @@ void TheoryProxy::getSkolems(TNode node,
 void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); }
 
 }  // namespace prop
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index dedd1fa49..3b21bde58 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -35,7 +35,7 @@
 #include "theory/trust_node.h"
 #include "util/resource_manager.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 class DecisionEngine;
 class TheoryEngine;
@@ -167,6 +167,6 @@ class TheoryProxy : public Registrar
 
 }  // namespace prop
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__PROP__SAT_H */