13 files changed, 27 insertions, 27 deletions
diff --git a/src/theory/bv/bitblast/aig_bitblaster.cpp b/src/theory/bv/bitblast/aig_bitblaster.cpp
index 002a4f631..fb5adb54c 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.cpp
+++ b/src/theory/bv/bitblast/aig_bitblaster.cpp
@@ -40,7 +40,7 @@ static inline int Cnf_Lit2Var(int Lit)
   return (Lit & 1) ? -(Lit >> 1) - 1 : (Lit >> 1) + 1;
 }
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -123,7 +123,7 @@ Abc_Ntk_t* AigBitblaster::currentAigNtk() {
   if (!AigBitblaster::s_abcAigNetwork) {
     Abc_Start();
     s_abcAigNetwork = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1);
-    char pName[] = "CVC5::theory::bv::AigNetwork";
+    char pName[] = "cvc5::theory::bv::AigNetwork";
     s_abcAigNetwork->pName = Extra_UtilStrsav(pName);
   }
   
@@ -496,5 +496,5 @@ AigBitblaster::Statistics::~Statistics() {
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 #endif // CVC4_USE_ABC
diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
index 3eccbd3ec..002ca71ec 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -33,7 +33,7 @@ typedef Abc_Aig_t_ Abc_Aig_t;
 class Cnf_Dat_t_;
 typedef Cnf_Dat_t_ Cnf_Dat_t;
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 class SatSolver;
 }
@@ -121,6 +121,6 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*>
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif  //  CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h
index 7ae55015f..72b079321 100644
--- a/src/theory/bv/bitblast/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast/bitblast_strategies_template.h
@@ -27,7 +27,7 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 namespace theory {
 namespace bv {
@@ -899,6 +899,6 @@ void DefaultRotateLeftBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb)
 
 }
 }
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
diff --git a/src/theory/bv/bitblast/bitblast_utils.h b/src/theory/bv/bitblast/bitblast_utils.h
index e342d4410..461d7fcaf 100644
--- a/src/theory/bv/bitblast/bitblast_utils.h
+++ b/src/theory/bv/bitblast/bitblast_utils.h
@@ -23,7 +23,7 @@
 #include <ostream>
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -267,6 +267,6 @@ T inline sLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqu
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif  // CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index 90ea5ac2b..311d44c94 100644
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -35,7 +35,7 @@
 #include "theory/valuation.h"
 #include "util/resource_manager.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -268,6 +268,6 @@ Node TBitblaster<T>::getTermModel(TNode node, bool fullModel)
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__THEORY__BV__BITBLAST__BITBLASTER_H */
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 5e22262e2..41fadd8b0 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -27,7 +27,7 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/theory_model.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -288,4 +288,4 @@ bool EagerBitblaster::isSharedTerm(TNode node) {
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index dead462b5..87699df40 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -26,7 +26,7 @@
 
 #include "prop/sat_solver.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -85,5 +85,5 @@ class BitblastingRegistrar : public prop::Registrar
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 #endif  //  CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index e20a6f6b5..a5d3e9bb6 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -30,7 +30,7 @@
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -590,4 +590,4 @@ void TLazyBitblaster::clearSolver() {
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index 1a963e67d..91995b56b 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -26,7 +26,7 @@
 #include "prop/bv_sat_solver_notify.h"
 #include "theory/bv/abstraction.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
 class CnfStream;
 class NullRegistrat;
@@ -176,5 +176,5 @@ class TLazyBitblaster : public TBitblaster<Node>
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 #endif  //  CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp
index b0cf68609..a441e769e 100644
--- a/src/theory/bv/bitblast/proof_bitblaster.cpp
+++ b/src/theory/bv/bitblast/proof_bitblaster.cpp
@@ -17,7 +17,7 @@
 
 #include "theory/theory_model.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -84,4 +84,4 @@ bool BBProof::collectModelValues(TheoryModel* m,
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h
index 894a9a916..4983b485e 100644
--- a/src/theory/bv/bitblast/proof_bitblaster.h
+++ b/src/theory/bv/bitblast/proof_bitblaster.h
@@ -18,7 +18,7 @@
 
 #include "theory/bv/bitblast/simple_bitblaster.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -47,5 +47,5 @@ class BBProof
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 #endif
diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp
index 76677e2db..05227ed09 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.cpp
+++ b/src/theory/bv/bitblast/simple_bitblaster.cpp
@@ -17,7 +17,7 @@
 #include "theory/theory_model.h"
 #include "theory/theory_state.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -155,4 +155,4 @@ bool BBSimple::isVariable(TNode node)
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h
index 1b48f9a68..300b93b53 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.h
+++ b/src/theory/bv/bitblast/simple_bitblaster.h
@@ -19,7 +19,7 @@
 
 #include "theory/bv/bitblast/bitblaster.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace theory {
 namespace bv {
 
@@ -75,6 +75,6 @@ class BBSimple : public TBitblaster<Node>
 
 }  // namespace bv
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif