Rename namespace CVC4 to CVC5. (#6249)

69 files changed, 482 insertions, 434 deletions

diff --git a/src/prop/README.minisat b/src/prop/README.minisat
index 2f1d8bb47..081e79191 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 CVC4::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 9a303a514..1645a096a 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 CVC4 {
+namespace CVC5 {
 namespace prop {
 
 class BVSatSolverNotify {
@@ -45,6 +45,6 @@ public:
 };/* class BVSatSolverInterface::Notify */
 
 }
-}
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index e58060191..fb764631f 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 CVC4 {
+namespace CVC5 {
 namespace prop {
 
 BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name)
@@ -297,5 +297,5 @@ void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
   d_statEliminatedVars.set(minisat->eliminated_vars);
 }
 
-} /* namespace CVC4::prop */
-} /* namespace CVC4 */
+}  // namespace prop
+} // namespace CVC5
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index f91ed4d1d..2a099ad21 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 CVC4 {
+namespace CVC5 {
 namespace prop {
 
 class BVMinisatSatSolver : public BVSatSolverInterface,
@@ -147,5 +147,5 @@ public:
   Statistics d_statistics;
 };
 
-} /* CVC4::prop namespace */
-} /* CVC4 namespace */
+}  // namespace prop
+}  // namespace CVC5
diff --git a/src/prop/bvminisat/core/Dimacs.h b/src/prop/bvminisat/core/Dimacs.h
index c94f473a9..be82fb557 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 CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -85,7 +85,7 @@ static void parse_DIMACS(gzFile input_stream, Solver& S) {
     parse_DIMACS_main(in, S); }
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 3b2b814cd..d7dc3f6d4 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 CVC4 {
+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(CVC4::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 (!CVC4::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 CVC4::theory::Interrupted& e)
+      catch (const CVC5::theory::Interrupted& e)
       {
         // do some clean-up and rethrow
         cancelUntil(assumptions.size());
@@ -1417,5 +1417,5 @@ bool Solver::withinBudget(ResourceManager::Resource r) const
           propagations < (uint64_t)propagation_budget);
 }
 
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 03c46985b..6386c33fa 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 CVC4 {
+namespace CVC5 {
 
 namespace BVMinisat {
 class Solver;
@@ -80,7 +80,7 @@ private:
     Notify* d_notify;
 
     /** Cvc4 context */
-    CVC4::context::Context* c;
+    CVC5::context::Context* c;
 
     /** True constant */
     Var varTrue;
@@ -92,138 +92,175 @@ public:
 
     // Constructor/Destructor:
     //
-    Solver(CVC4::context::Context* c);
-    virtual ~Solver();
-
-    void setNotify(Notify* toNotify);
-
-    // Problem specification:
-    //
-    Var     newVar    (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
-    Var     trueVar() const { return varTrue; }
-    Var     falseVar() const { return varFalse; }
-
-    bool addClause(const vec<Lit>& ps,
-                   ClauseId& id);  // Add a clause to the solver.
-    bool    addEmptyClause();                                   // Add the empty clause, making the solver contradictory.
-    bool addClause(Lit p, ClauseId& id);  // Add a unit clause to the solver.
-    bool addClause(Lit p,
-                   Lit q,
-                   ClauseId& id);  // Add a binary clause to the solver.
-    bool addClause(Lit p,
-                   Lit q,
-                   Lit r,
-                   ClauseId& id);  // Add a ternary clause to the solver.
-    bool    addClause_(      vec<Lit>& ps, ClauseId& id);                     // Add a clause to the solver without making superflous internal copy. Will
-                                                                // change the passed vector 'ps'.
-
-    // Solving:
-    //
-    bool    simplify     ();                        // Removes already satisfied clauses.
-    lbool    solve        (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions.
-    lbool   solveLimited (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions (With resource constraints).
-    lbool    solve        ();                        // Search without assumptions.
-    lbool    solve        (Lit p);                   // Search for a model that respects a single assumption.
-    lbool    solve        (Lit p, Lit q);            // Search for a model that respects two assumptions.
-    lbool    solve        (Lit p, Lit q, Lit r);     // Search for a model that respects three assumptions.
-    bool    okay         () const;                  // FALSE means solver is in a conflicting state
-    lbool   assertAssumption(Lit p, bool propagate);  // Assert a new assumption, start BCP if propagate = true
-    lbool   propagateAssumptions();                   // Do BCP over asserted assumptions
-    void    popAssumption();                          // Pop an assumption
-
-    void    toDimacs     (FILE* f, const vec<Lit>& assumps);            // Write CNF to file in DIMACS-format.
-    void    toDimacs     (const char *file, const vec<Lit>& assumps);
-    void    toDimacs     (FILE* f, Clause& c, vec<Var>& map, Var& max);
-
-    // Convenience versions of 'toDimacs()':
-    void    toDimacs     (const char* file);
-    void    toDimacs     (const char* file, Lit p);
-    void    toDimacs     (const char* file, Lit p, Lit q);
-    void    toDimacs     (const char* file, Lit p, Lit q, Lit r);
-
-    // Variable mode:
-    //
-    void    setPolarity    (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
-    void    setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
-
-    // Read state:
-    //
-    lbool   value      (Var x) const;       // The current value of a variable.
-    lbool   value      (Lit p) const;       // The current value of a literal.
-    lbool   modelValue (Var x) const;       // The value of a variable in the last model. The last call to solve must have been satisfiable.
-    lbool   modelValue (Lit p) const;       // The value of a literal in the last model. The last call to solve must have been satisfiable.
-    int     nAssigns   ()      const;       // The current number of assigned literals.
-    int     nClauses   ()      const;       // The current number of original clauses.
-    int     nLearnts   ()      const;       // The current number of learnt clauses.
-    int     nVars      ()      const;       // The current number of variables.
-    int     nFreeVars  ()      const;
-
-    // Resource contraints:
-    //
-    void    setConfBudget(int64_t x);
-    void    setPropBudget(int64_t x);
-    void    budgetOff();
-    void    interrupt();          // Trigger a (potentially asynchronous) interruption of the solver.
-    void    clearInterrupt();     // Clear interrupt indicator flag.
-
-    // Memory managment:
-    //
-    virtual void garbageCollect();
-    void    checkGarbage(double gf);
-    void    checkGarbage();
-
-    // Extra results: (read-only member variable)
-    //
-    vec<lbool> model;             // If problem is satisfiable, this vector contains the model (if any).
-    vec<Lit>   conflict;          // If problem is unsatisfiable (possibly under assumptions),
-                                  // this vector represent the final conflict clause expressed in the assumptions.
-
-    // Mode of operation:
-    //
-    int       verbosity;
-    double    var_decay;
-    double    clause_decay;
-    double    random_var_freq;
-    double    random_seed;
-    bool      luby_restart;
-    int       ccmin_mode;         // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
-    int       phase_saving;       // Controls the level of phase saving (0=none, 1=limited, 2=full).
-    bool      rnd_pol;            // Use random polarities for branching heuristics.
-    bool      rnd_init_act;       // Initialize variable activities with a small random value.
-    double    garbage_frac;       // The fraction of wasted memory allowed before a garbage collection is triggered.
-
-    int       restart_first;      // The initial restart limit.                                                                (default 100)
-    double    restart_inc;        // The factor with which the restart limit is multiplied in each restart.                    (default 1.5)
-    double    learntsize_factor;  // The intitial limit for learnt clauses is a factor of the original clauses.                (default 1 / 3)
-    double    learntsize_inc;     // The limit for learnt clauses is multiplied with this factor each restart.                 (default 1.1)
-
-    int       learntsize_adjust_start_confl;
-    double    learntsize_adjust_inc;
-
-    // Statistics: (read-only member variable)
-    //
-    uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts;
-    uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
-
-    // Bitvector Propagations
-    //
-
-    void addMarkerLiteral(Var var);
-
-    bool need_to_propagate;  // true if we added new clauses, set to true in
-                             // propagation
-    bool only_bcp;                      // solving mode in which only boolean constraint propagation is done
-    void setOnlyBCP (bool val) { only_bcp = val;}
-    void explain(Lit l, std::vector<Lit>& explanation);
-
-   protected:
-
-    // has a clause been added
-    bool                clause_added;
-
-    // Helper structures:
-    //
-    struct VarData { CRef reason; int level; };
+ Solver(CVC5::context::Context* c);
+ virtual ~Solver();
+
+ void setNotify(Notify* toNotify);
+
+ // Problem specification:
+ //
+ Var newVar(bool polarity = true,
+            bool dvar = true);  // Add a new variable with parameters specifying
+                                // variable mode.
+ Var trueVar() const { return varTrue; }
+ Var falseVar() const { return varFalse; }
+
+ bool addClause(const vec<Lit>& ps,
+                ClauseId& id);  // Add a clause to the solver.
+ bool addEmptyClause();         // Add the empty clause, making the solver
+                                // contradictory.
+ bool addClause(Lit p, ClauseId& id);  // Add a unit clause to the solver.
+ bool addClause(Lit p,
+                Lit q,
+                ClauseId& id);  // Add a binary clause to the solver.
+ bool addClause(Lit p,
+                Lit q,
+                Lit r,
+                ClauseId& id);  // Add a ternary clause to the solver.
+ bool addClause_(
+     vec<Lit>& ps,
+     ClauseId& id);  // Add a clause to the solver without making superflous
+                     // internal copy. Will change the passed vector 'ps'.
+
+ // Solving:
+ //
+ bool simplify();                       // Removes already satisfied clauses.
+ lbool solve(const vec<Lit>& assumps);  // Search for a model that respects a
+                                        // given set of assumptions.
+ lbool solveLimited(
+     const vec<Lit>& assumps);  // Search for a model that respects a given set
+                                // of assumptions (With resource constraints).
+ lbool solve();                 // Search without assumptions.
+ lbool solve(Lit p);  // Search for a model that respects a single assumption.
+ lbool solve(Lit p,
+             Lit q);  // Search for a model that respects two assumptions.
+ lbool solve(Lit p,
+             Lit q,
+             Lit r);  // Search for a model that respects three assumptions.
+ bool okay() const;   // FALSE means solver is in a conflicting state
+ lbool assertAssumption(
+     Lit p,
+     bool propagate);  // Assert a new assumption, start BCP if propagate = true
+ lbool propagateAssumptions();  // Do BCP over asserted assumptions
+ void popAssumption();          // Pop an assumption
+
+ void toDimacs(FILE* f,
+               const vec<Lit>& assumps);  // Write CNF to file in DIMACS-format.
+ void toDimacs(const char* file, const vec<Lit>& assumps);
+ void toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max);
+
+ // Convenience versions of 'toDimacs()':
+ void toDimacs(const char* file);
+ void toDimacs(const char* file, Lit p);
+ void toDimacs(const char* file, Lit p, Lit q);
+ void toDimacs(const char* file, Lit p, Lit q, Lit r);
+
+ // Variable mode:
+ //
+ void setPolarity(
+     Var v, bool b);  // Declare which polarity the decision heuristic should
+                      // use for a variable. Requires mode 'polarity_user'.
+ void setDecisionVar(Var v,
+                     bool b);  // Declare if a variable should be eligible for
+                               // selection in the decision heuristic.
+
+ // Read state:
+ //
+ lbool value(Var x) const;  // The current value of a variable.
+ lbool value(Lit p) const;  // The current value of a literal.
+ lbool modelValue(
+     Var x) const;  // The value of a variable in the last model. The last call
+                    // to solve must have been satisfiable.
+ lbool modelValue(
+     Lit p) const;  // The value of a literal in the last model. The last call
+                    // to solve must have been satisfiable.
+ int nAssigns() const;  // The current number of assigned literals.
+ int nClauses() const;  // The current number of original clauses.
+ int nLearnts() const;  // The current number of learnt clauses.
+ int nVars() const;     // The current number of variables.
+ int nFreeVars() const;
+
+ // Resource contraints:
+ //
+ void setConfBudget(int64_t x);
+ void setPropBudget(int64_t x);
+ void budgetOff();
+ void interrupt();  // Trigger a (potentially asynchronous) interruption of the
+                    // solver.
+ void clearInterrupt();  // Clear interrupt indicator flag.
+
+ // Memory managment:
+ //
+ virtual void garbageCollect();
+ void checkGarbage(double gf);
+ void checkGarbage();
+
+ // Extra results: (read-only member variable)
+ //
+ vec<lbool> model;  // If problem is satisfiable, this vector contains the model
+                    // (if any).
+ vec<Lit> conflict;  // If problem is unsatisfiable (possibly under
+                     // assumptions), this vector represent the final conflict
+                     // clause expressed in the assumptions.
+
+ // Mode of operation:
+ //
+ int verbosity;
+ double var_decay;
+ double clause_decay;
+ double random_var_freq;
+ double random_seed;
+ bool luby_restart;
+ int ccmin_mode;    // Controls conflict clause minimization (0=none, 1=basic,
+                    // 2=deep).
+ int phase_saving;  // Controls the level of phase saving (0=none, 1=limited,
+                    // 2=full).
+ bool rnd_pol;      // Use random polarities for branching heuristics.
+ bool
+     rnd_init_act;  // Initialize variable activities with a small random value.
+ double garbage_frac;  // The fraction of wasted memory allowed before a garbage
+                       // collection is triggered.
+
+ int restart_first;   // The initial restart limit. (default 100)
+ double restart_inc;  // The factor with which the restart limit is multiplied
+                      // in each restart.                    (default 1.5)
+ double
+     learntsize_factor;  // The intitial limit for learnt clauses is a factor of
+                         // the original clauses.                (default 1 / 3)
+ double learntsize_inc;  // The limit for learnt clauses is multiplied with this
+                         // factor each restart.                 (default 1.1)
+
+ int learntsize_adjust_start_confl;
+ double learntsize_adjust_inc;
+
+ // Statistics: (read-only member variable)
+ //
+ uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts;
+ uint64_t dec_vars, clauses_literals, learnts_literals, max_literals,
+     tot_literals;
+
+ // Bitvector Propagations
+ //
+
+ void addMarkerLiteral(Var var);
+
+ bool need_to_propagate;  // true if we added new clauses, set to true in
+                          // propagation
+ bool only_bcp;  // solving mode in which only boolean constraint propagation is
+                 // done
+ void setOnlyBCP(bool val) { only_bcp = val; }
+ void explain(Lit l, std::vector<Lit>& explanation);
+
+protected:
+ // has a clause been added
+ bool clause_added;
+
+ // Helper structures:
+ //
+ struct VarData
+ {
+   CRef reason;
+   int level; };
     static inline VarData mkVarData(CRef cr, int l){ VarData d = {cr, l}; return d; }
 
     struct Watcher {
@@ -496,8 +533,7 @@ inline void     Solver::toDimacs     (const char* file, Lit p, Lit q, Lit r){ ve
 
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
-
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/core/SolverTypes.h b/src/prop/bvminisat/core/SolverTypes.h
index 776052848..96022efbf 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 CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 class Solver;
 }
 template <class Solver>
 class TSatProof;
-}
+}  // namespace CVC5
 
-namespace CVC4 {
+namespace CVC5 {
 
 namespace BVMinisat {
 
@@ -429,7 +429,7 @@ inline void Clause::strengthen(Lit p)
 
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Alg.h b/src/prop/bvminisat/mtl/Alg.h
index 5918b2f4c..0b173eb08 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 CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -81,7 +81,7 @@ template<class T>
 static inline void append(const vec<T>& from, vec<T>& to){ copy(from, to, true); }
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Alloc.h b/src/prop/bvminisat/mtl/Alloc.h
index 8a03caa69..582db74f1 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 CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -148,7 +148,7 @@ RegionAllocator<T>::alloc(int size)
 
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Heap.h b/src/prop/bvminisat/mtl/Heap.h
index 38b47bc7f..7b04a5091 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 CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -155,8 +155,7 @@ class Heap {
 
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
-
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Map.h b/src/prop/bvminisat/mtl/Map.h
index 919149fa9..fd64fc751 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 CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -190,7 +190,7 @@ class Map {
 };
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Queue.h b/src/prop/bvminisat/mtl/Queue.h
index 1120188f8..a72660337 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 CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -85,7 +85,7 @@ public:
 
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Sort.h b/src/prop/bvminisat/mtl/Sort.h
index f4a10aabb..1cfa220ab 100644
--- a/src/prop/bvminisat/mtl/Sort.h
+++ b/src/prop/bvminisat/mtl/Sort.h
@@ -26,8 +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 CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 template<class T>
@@ -94,7 +93,7 @@ template <class T> void sort(vec<T>& v) {
 
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/Vec.h b/src/prop/bvminisat/mtl/Vec.h
index a6e3bca4b..c918fc4a0 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 CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -146,7 +146,7 @@ void vec<T>::clear(bool dealloc) {
         if (dealloc) free(data), data = NULL, cap = 0; } }
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/mtl/XAlloc.h b/src/prop/bvminisat/mtl/XAlloc.h
index 9e469a6fb..1500114a2 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 CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //=================================================================================================
@@ -41,8 +41,7 @@ static inline void* xrealloc(void *ptr, size_t size)
 }
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
-
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index 10f0aa03e..b4f9bd354 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 CVC4 {
+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(CVC4::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(CVC4::context::Context* context)
       use_asymm(opt_use_asymm),
       use_rcheck(opt_use_rcheck),
       use_elim(opt_use_elim
-               && CVC4::options::bitblastMode()
-                      == CVC4::options::BitblastMode::EAGER
-               && !CVC4::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(CVC4::context::Context* context)
 
 SimpSolver::~SimpSolver()
 {
-  //  CVC4::StatisticsRegistry::unregisterStat(&total_eliminate_time);
+  //  CVC5::StatisticsRegistry::unregisterStat(&total_eliminate_time);
 }
 
 
@@ -644,64 +644,77 @@ void SimpSolver::extendModel()
 
 bool SimpSolver::eliminate(bool turn_off_elim)
 {
+  //  CVC5::TimerStat::CodeTimer codeTimer(total_eliminate_time);
 
-  //  CVC4::TimerStat::CodeTimer codeTimer(total_eliminate_time);
-
-    if (!simplify())
-        return false;
-    else if (!use_simplification)
-        return true;
-
-    // Main simplification loop:
-    //
-    while (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0){
+  if (!simplify())
+    return false;
+  else if (!use_simplification)
+    return true;
 
-        gatherTouchedClauses();
-        // printf("  ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
-        if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size())
-            && !backwardSubsumptionCheck(true))
-        {
-          ok = false;
-          goto cleanup;
-        }
+  // Main simplification loop:
+  //
+  while (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0)
+  {
+    gatherTouchedClauses();
+    // printf("  ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n",
+    // cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
+    if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size())
+        && !backwardSubsumptionCheck(true))
+    {
+      ok = false;
+      goto cleanup;
+    }
 
-        // Empty elim_heap and return immediately on user-interrupt:
-        if (asynch_interrupt){
-          Assert(bwdsub_assigns == trail.size());
-          Assert(subsumption_queue.size() == 0);
-          Assert(n_touched == 0);
-          elim_heap.clear();
-          goto cleanup;
-        }
+    // Empty elim_heap and return immediately on user-interrupt:
+    if (asynch_interrupt)
+    {
+      Assert(bwdsub_assigns == trail.size());
+      Assert(subsumption_queue.size() == 0);
+      Assert(n_touched == 0);
+      elim_heap.clear();
+      goto cleanup;
+    }
 
-        // printf("  ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
-        for (int cnt = 0; !elim_heap.empty(); cnt++){
-            Var elim = elim_heap.removeMin();
+    // printf("  ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(),
+    // elim_heap.size());
+    for (int cnt = 0; !elim_heap.empty(); cnt++)
+    {
+      Var elim = elim_heap.removeMin();
 
-            if (asynch_interrupt) break;
+      if (asynch_interrupt) break;
 
-            if (isEliminated(elim) || value(elim) != l_Undef) continue;
+      if (isEliminated(elim) || value(elim) != l_Undef) continue;
 
-            if (verbosity >= 2 && cnt % 100 == 0)
-                printf("elimination left: %10d\r", elim_heap.size());
+      if (verbosity >= 2 && cnt % 100 == 0)
+        printf("elimination left: %10d\r", elim_heap.size());
 
-            if (use_asymm){
-                // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
-                bool was_frozen = frozen[elim];
-                frozen[elim] = true;
-                if (!asymmVar(elim)){
-                    ok = false; goto cleanup; }
-                frozen[elim] = was_frozen; }
+      if (use_asymm)
+      {
+        // Temporarily freeze variable. Otherwise, it would immediately end up
+        // on the queue again:
+        bool was_frozen = frozen[elim];
+        frozen[elim] = true;
+        if (!asymmVar(elim))
+        {
+          ok = false;
+          goto cleanup;
+        }
+        frozen[elim] = was_frozen;
+      }
 
-            // At this point, the variable may have been set by assymetric branching, so check it
-            // again. Also, don't eliminate frozen variables:
-            if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){
-                ok = false; goto cleanup; }
+      // At this point, the variable may have been set by assymetric branching,
+      // so check it again. Also, don't eliminate frozen variables:
+      if (use_elim && value(elim) == l_Undef && !frozen[elim]
+          && !eliminateVar(elim))
+      {
+        ok = false;
+        goto cleanup;
+      }
 
-            checkGarbage(simp_garbage_frac);
-        }
+      checkGarbage(simp_garbage_frac);
+    }
 
-        Assert(subsumption_queue.size() == 0);
+    Assert(subsumption_queue.size() == 0);
     }
  cleanup:
 
@@ -795,5 +808,5 @@ void SimpSolver::garbageCollect()
     to.moveTo(ca);
 }
 
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h
index bf23a7dff..6afdc6ba7 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 CVC4 {
+namespace CVC5 {
 
 namespace context {
 class Context;
@@ -41,7 +41,7 @@ class SimpSolver : public Solver {
  public:
     // Constructor/Destructor:
     //
-  SimpSolver(CVC4::context::Context* context);
+  SimpSolver(CVC5::context::Context* context);
   ~SimpSolver();
 
   // Problem specification:
@@ -115,9 +115,9 @@ class SimpSolver : public Solver {
     int     merges;
     int     asymm_lits;
     int     eliminated_vars;
-  //    CVC4::TimerStat total_eliminate_time;
+    //    CVC5::TimerStat total_eliminate_time;
 
- protected:
+   protected:
 
     // Helper structures:
     //
@@ -237,8 +237,7 @@ inline lbool SimpSolver::solveLimited (bool do_simp, bool turn_off_simp){
     return solve_(do_simp, turn_off_simp); }
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
-
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/utils/Options.cc b/src/prop/bvminisat/utils/Options.cc
index ac0964623..44c642441 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 CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 void BVMinisat::parseOptions(int& argc, char** argv, bool strict)
@@ -90,6 +90,5 @@ void BVMinisat::printUsageAndExit (int argc, char** argv, bool verbose)
     exit(0);
 }
 
-
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
diff --git a/src/prop/bvminisat/utils/Options.h b/src/prop/bvminisat/utils/Options.h
index 698035b7c..e7b6942bd 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 CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //==================================================================================================
@@ -431,7 +431,7 @@ class BoolOption : public Option
 };
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/utils/ParseUtils.h b/src/prop/bvminisat/utils/ParseUtils.h
index 46f404c3e..a748651db 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 CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 //-------------------------------------------------------------------------------------------------
@@ -119,7 +119,7 @@ static bool eagerMatch(B& in, const char* str) {
 
 
 //=================================================================================================
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/bvminisat/utils/System.cc b/src/prop/bvminisat/utils/System.cc
index aba0a5ac5..9b9f99eb5 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 CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 // TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and
@@ -95,6 +95,5 @@ double BVMinisat::memUsed() {
     return 0; }
 #endif
 
-
-} /* CVC4::BVMinisat namespace */
+} /* CVC5::BVMinisat namespace */
 } /* CVC4 namespace */
diff --git a/src/prop/bvminisat/utils/System.h b/src/prop/bvminisat/utils/System.h
index 6a887bdb0..117fbfa3d 100644
--- a/src/prop/bvminisat/utils/System.h
+++ b/src/prop/bvminisat/utils/System.h
@@ -29,15 +29,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 //-------------------------------------------------------------------------------------------------
 
-namespace CVC4 {
+namespace CVC5 {
 namespace BVMinisat {
 
 static inline double cpuTime(void); // CPU-time in seconds.
 extern double memUsed();            // Memory in mega bytes (returns 0 for unsupported architectures).
 extern double memUsedPeak();        // Peak-memory in mega bytes (returns 0 for unsupported architectures).
 
-} /* CVC4::BVMinisat namespace */
-} /* CVC4 namespace */
+}  // namespace BVMinisat
+}  // namespace CVC5
 
 //-------------------------------------------------------------------------------------------------
 // Implementation of inline functions:
@@ -45,17 +45,22 @@ extern double memUsedPeak();        // Peak-memory in mega bytes (returns 0 for
 #if defined(_MSC_VER) || defined(__MINGW32__)
 #include <time.h>
 
-static inline double CVC4::BVMinisat::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; }
+static inline double CVC5::BVMinisat::cpuTime(void)
+{
+  return (double)clock() / CLOCKS_PER_SEC;
+}
 
 #else
 #include <sys/time.h>
 #include <sys/resource.h>
 #include <unistd.h>
 
-static inline double CVC4::BVMinisat::cpuTime(void) {
-    struct rusage ru;
-    getrusage(RUSAGE_SELF, &ru);
-    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
+static inline double CVC5::BVMinisat::cpuTime(void)
+{
+  struct rusage ru;
+  getrusage(RUSAGE_SELF, &ru);
+  return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000;
+}
 
 #endif
 
diff --git a/src/prop/cadical.cpp b/src/prop/cadical.cpp
index 6020efad1..9bad7072a 100644
--- a/src/prop/cadical.cpp
+++ b/src/prop/cadical.cpp
@@ -20,7 +20,7 @@
 
 #include "base/check.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace prop {
 
 using CadicalLit = int;
@@ -200,6 +200,6 @@ CadicalSolver::Statistics::~Statistics() {
 }
 
 }  // namespace prop
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif  // CVC4_USE_CADICAL
diff --git a/src/prop/cadical.h b/src/prop/cadical.h
index dfd761e2e..c49aa8d03 100644
--- a/src/prop/cadical.h
+++ b/src/prop/cadical.h
@@ -26,7 +26,7 @@
 
 #include <cadical.hpp>
 
-namespace CVC4 {
+namespace CVC5 {
 namespace prop {
 
 class CadicalSolver : public SatSolver
@@ -103,7 +103,7 @@ class CadicalSolver : public SatSolver
 };
 
 }  // namespace prop
-}  // namespace CVC4
+}  // 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 8cd4da505..bd23bad94 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 CVC4 {
+namespace CVC5 {
 namespace prop {
 
 CnfStream::CnfStream(SatSolver* satSolver,
@@ -787,5 +787,5 @@ void CnfStream::convertAndAssert(TNode node, bool negated)
   }
 }
 
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+}  // namespace prop
+}  // namespace CVC5
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 1a900a524..af86da746 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 CVC4 {
+namespace CVC5 {
 
 class OutputManager;
 
@@ -318,6 +318,6 @@ class CnfStream {
 }; /* class CnfStream */
 
 }  // namespace prop
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PROP__CNF_STREAM_H */
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index d81429d44..91fc12c6c 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -22,7 +22,7 @@
 
 #include <cryptominisat5/cryptominisat.h>
 
-namespace CVC4 {
+namespace CVC5 {
 namespace prop {
 
 using CMSatVar = unsigned;
@@ -244,5 +244,5 @@ CryptoMinisatSolver::Statistics::~Statistics() {
 }
 
 }  // namespace prop
-}  // namespace CVC4
+}  // namespace CVC5
 #endif
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index 3bb443cfc..fb118619c 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -33,7 +33,7 @@ namespace CMSat {
   class SATSolver;
 }
 
-namespace CVC4 {
+namespace CVC5 {
 namespace prop {
 
 class CryptoMinisatSolver : public SatSolver
@@ -106,7 +106,7 @@ class CryptoMinisatSolver : public SatSolver
 };
 
 }  // namespace prop
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif  // CVC4_USE_CRYPTOMINISAT
 #endif  // CVC4__PROP__CRYPTOMINISAT_H
diff --git a/src/prop/kissat.cpp b/src/prop/kissat.cpp
index 7ff6d76ee..ccca3a3b4 100644
--- a/src/prop/kissat.cpp
+++ b/src/prop/kissat.cpp
@@ -20,7 +20,7 @@
 
 #include "base/check.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace prop {
 
 using KissatLit = int32_t;
@@ -173,6 +173,6 @@ KissatSolver::Statistics::~Statistics()
 }
 
 }  // namespace prop
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif  // CVC4_USE_KISSAT
diff --git a/src/prop/kissat.h b/src/prop/kissat.h
index 65088e39e..7bfcbac68 100644
--- a/src/prop/kissat.h
+++ b/src/prop/kissat.h
@@ -28,7 +28,7 @@ extern "C" {
 #include <kissat/kissat.h>
 }
 
-namespace CVC4 {
+namespace CVC5 {
 namespace prop {
 
 class KissatSolver : public SatSolver
@@ -97,7 +97,7 @@ class KissatSolver : public SatSolver
 };
 
 }  // namespace prop
-}  // namespace CVC4
+}  // 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 e4728f6b6..b48044457 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 CVC4 {
+namespace CVC5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -86,6 +86,6 @@ static void parse_DIMACS(gzFile input_stream, Solver& S) {
 
 //=================================================================================================
 }
-}
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 8c27e2bdd..9dbcada15 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 CVC4::prop;
+using namespace CVC5::prop;
 
-namespace CVC4 {
+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,
-                                               CVC4::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,
-                                            CVC4::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(CVC4::prop::TheoryProxy* proxy,
-               CVC4::context::Context* context,
-               CVC4::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(
-                  CVC4::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(
-                    CVC4::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") << CVC4::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") << CVC4::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(CVC4::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(CVC4::theory::Theory::EFFORT_FULL);
+              theoryCheck(CVC5::theory::Theory::EFFORT_FULL);
             } else {
-              theoryCheck(CVC4::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(CVC4::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"
-                   << CVC4::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") << CVC4::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,
-                            CVC4::TSatProof<Solver>* proof)
+                            CVC5::TSatProof<Solver>* proof)
 {
   Debug("minisat") << "ClauseAllocator::reloc: cr " << cr << std::endl;
   // FIXME what is this CRef_lazy
@@ -2397,5 +2397,5 @@ std::shared_ptr<ProofNode> Solver::getProof()
 
 bool Solver::isProofEnabled() const { return d_pfManager != nullptr; }
 
-} /* CVC4::Minisat namespace */
-} /* CVC4 namespace */
+}  // namespace Minisat
+}  // namespace CVC5
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index df2f9b967..53f7a828c 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -38,17 +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 CVC4 {
+namespace CVC5 {
 template <class Solver> class TSatProof;
 
 namespace prop {
 class PropEngine;
 class TheoryProxy;
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+}  // namespace prop
+}  // namespace CVC5
 
-
-namespace CVC4 {
+namespace CVC5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -57,12 +56,12 @@ namespace Minisat {
 class Solver {
 
   /** The only two CVC4 entry points to the private solver data */
-  friend class CVC4::prop::PropEngine;
-  friend class CVC4::prop::TheoryProxy;
-  friend class CVC4::prop::SatProofManager;
-  friend class CVC4::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:
+ public:
   static CRef TCRef_Undef;
   static CRef TCRef_Lazy;
 
@@ -74,10 +73,10 @@ public:
 
  protected:
   /** The pointer to the proxy that provides interfaces to the SMT engine */
-  CVC4::prop::TheoryProxy* d_proxy;
+  CVC5::prop::TheoryProxy* d_proxy;
 
   /** The context from the SMT solver */
-  CVC4::context::Context* d_context;
+  CVC5::context::Context* d_context;
 
   /** The current assertion level (user) */
   int assertionLevel;
@@ -89,7 +88,7 @@ public:
   Var varFalse;
 
   /** The resolution proof manager */
-  std::unique_ptr<CVC4::prop::SatProofManager> d_pfManager;
+  std::unique_ptr<CVC5::prop::SatProofManager> d_pfManager;
 
  public:
   /** Returns the current user assertion level */
@@ -106,7 +105,7 @@ public:
   vec<bool> lemmas_removable;
 
   /** Nodes being converted to CNF */
-  std::vector<CVC4::Node> lemmas_cnf_assertion;
+  std::vector<CVC5::Node> lemmas_cnf_assertion;
 
   /** Do a another check if FULL_EFFORT was the last one */
   bool recheck;
@@ -135,9 +134,9 @@ public:
 
     // Constructor/Destructor:
     //
- Solver(CVC4::prop::TheoryProxy* proxy,
-        CVC4::context::Context* context,
-        CVC4::context::UserContext* userContext,
+ Solver(CVC5::prop::TheoryProxy* proxy,
+        CVC5::context::Context* context,
+        CVC5::context::UserContext* userContext,
         ProofNodeManager* pnm,
         bool enableIncremental = false);
  virtual ~Solver();
@@ -154,7 +153,7 @@ public:
  Var falseVar() const { return varFalse; }
 
  /** Retrive the SAT proof manager */
- CVC4::prop::SatProofManager* getProofManager();
+ CVC5::prop::SatProofManager* getProofManager();
 
  /** Retrive the refutation proof */
  std::shared_ptr<ProofNode> getProof();
@@ -438,7 +437,9 @@ protected:
     CRef     propagate        (TheoryCheckType type);                                  // Perform Boolean and Theory. Returns possibly conflicting clause.
     CRef     propagateBool    ();                                                      // Perform Boolean propagation. Returns possibly conflicting clause.
     void     propagateTheory  ();                                                      // Perform Theory propagation.
-    void     theoryCheck      (CVC4::theory::Theory::Effort effort);                   // Perform a theory satisfiability check. Adds lemmas.
+    void theoryCheck(
+        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.
     int      analyze          (CRef confl, vec<Lit>& out_learnt, int& out_btlevel);    // (bt = backtrack)
@@ -664,7 +665,7 @@ inline void     Solver::toDimacs     (const char* file, Lit p, Lit q, Lit r){ ve
 
 
 //=================================================================================================
-} /* CVC4::Minisat namespace */
-} /* CVC4 namespace */
+}  // namespace Minisat
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index f2d2860c8..4d9dd682d 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 CVC4 {
+namespace CVC5 {
 namespace Minisat {
 class Solver;
 }
 template <class Solver>
 class TSatProof;
-}  // namespace CVC4
+}  // namespace CVC5
 
-namespace CVC4 {
+namespace CVC5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -182,11 +182,10 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) {
   return out;
 }
 
-} /* namespace CVC4::Minisat */
-} /* namespace CVC4 */
+}  // namespace Minisat
+} // namespace CVC5
 
-
-namespace CVC4 {
+namespace CVC5 {
 namespace Minisat{
 
 //=================================================================================================
@@ -323,7 +322,7 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
 
     void reloc(CRef& cr,
                ClauseAllocator& to,
-               CVC4::TSatProof<Solver>* proof = NULL);
+               CVC5::TSatProof<Solver>* proof = NULL);
     // Implementation moved to Solver.cc.
 };
 
@@ -501,6 +500,6 @@ inline void Clause::strengthen(Lit p)
 
 //=================================================================================================
 }
-}
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 694c73e5e..e95677d57 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 CVC4 {
+namespace CVC5 {
 namespace prop {
 
 //// DPllMinisatSatSolver
@@ -300,20 +300,21 @@ void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){
   d_statTotLiterals.set(minisat->tot_literals);
 }
 
-} /* namespace CVC4::prop */
-} /* namespace CVC4 */
+}  // namespace prop
+} // namespace CVC5
 
-
-namespace CVC4 {
-template<>
-prop::SatLiteral toSatLiteral< CVC4::Minisat::Solver>(Minisat::Solver::TLit lit) {
+namespace CVC5 {
+template <>
+prop::SatLiteral toSatLiteral<CVC5::Minisat::Solver>(Minisat::Solver::TLit lit)
+{
   return prop::MinisatSatSolver::toSatLiteral(lit);
 }
 
-template<>
-void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& minisat_cl,
-                                      prop::SatClause& sat_cl) {
+template <>
+void toSatClause<CVC5::Minisat::Solver>(
+    const CVC5::Minisat::Solver::TClause& minisat_cl, prop::SatClause& sat_cl)
+{
   prop::MinisatSatSolver::toSatClause(minisat_cl, sat_cl);
 }
 
-} /* namespace CVC4 */
+} // namespace CVC5
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 472ded34e..7dfeb6aa2 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 CVC4 {
+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,
-                  CVC4::context::UserContext* userContext,
+                  CVC5::context::UserContext* userContext,
                   ProofNodeManager* pnm) override;
 
   ClauseId addClause(SatClause& clause, bool removable) override;
@@ -118,5 +118,5 @@ class MinisatSatSolver : public CDCLTSatSolverInterface
 
 }; /* class MinisatSatSolver */
 
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+}  // namespace prop
+}  // namespace CVC5
diff --git a/src/prop/minisat/mtl/Alg.h b/src/prop/minisat/mtl/Alg.h
index 2f8a86c3b..37bc4b7b6 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 CVC4 {
+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
 
 #endif
diff --git a/src/prop/minisat/mtl/Alloc.h b/src/prop/minisat/mtl/Alloc.h
index 98e59e7bf..850aaeb73 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 CVC4 {
+namespace CVC5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -149,6 +149,6 @@ RegionAllocator<T>::alloc(int size)
 
 //=================================================================================================
 }
-}
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/minisat/mtl/Heap.h b/src/prop/minisat/mtl/Heap.h
index 1e64f6ba5..e2ad1513f 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 CVC4 {
+namespace CVC5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -156,6 +156,6 @@ class Heap {
 
 //=================================================================================================
 }
-}
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/minisat/mtl/Map.h b/src/prop/minisat/mtl/Map.h
index bf299d55d..2efed4433 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 CVC4 {
+namespace CVC5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -191,6 +191,6 @@ class Map {
 
 //=================================================================================================
 }
-}
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/minisat/mtl/Queue.h b/src/prop/minisat/mtl/Queue.h
index 242bc9388..ef30591bf 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 CVC4 {
+namespace CVC5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -86,6 +86,6 @@ public:
 
 //=================================================================================================
 }
-}
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/minisat/mtl/Sort.h b/src/prop/minisat/mtl/Sort.h
index 2c3454aa3..7cf393847 100644
--- a/src/prop/minisat/mtl/Sort.h
+++ b/src/prop/minisat/mtl/Sort.h
@@ -26,8 +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 CVC4 {
+namespace CVC5 {
 namespace Minisat {
 
 template<class T>
@@ -95,6 +94,6 @@ template <class T> void sort(vec<T>& v) {
 
 //=================================================================================================
 }
-}
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/minisat/mtl/Vec.h b/src/prop/minisat/mtl/Vec.h
index 08e40e8bc..e17e320d2 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 CVC4 {
+namespace CVC5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -147,6 +147,6 @@ void vec<T>::clear(bool dealloc) {
 
 //=================================================================================================
 }
-}
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/minisat/mtl/XAlloc.h b/src/prop/minisat/mtl/XAlloc.h
index f1221f94f..6bd8c02e8 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 CVC4 {
+namespace CVC5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -42,6 +42,6 @@ static inline void* xrealloc(void *ptr, size_t size)
 
 //=================================================================================================
 }
-}
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 7051134eb..52162776b 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 CVC4;
-using namespace CVC4::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(CVC4::prop::TheoryProxy* proxy,
-                       CVC4::context::Context* context,
-                       CVC4::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 f553746e6..6c8a87d5e 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 CVC4 {
+namespace CVC5 {
 namespace prop {
   class TheoryProxy;
 }
-}
+}  // namespace CVC5
 
-namespace CVC4 {
+namespace CVC5 {
 namespace Minisat {
 
 //=================================================================================================
@@ -42,9 +42,9 @@ class SimpSolver : public Solver {
  public:
     // Constructor/Destructor:
     //
-  SimpSolver(CVC4::prop::TheoryProxy* proxy,
-             CVC4::context::Context* context,
-             CVC4::context::UserContext* userContext,
+  SimpSolver(CVC5::prop::TheoryProxy* proxy,
+             CVC5::context::Context* context,
+             CVC5::context::UserContext* userContext,
              ProofNodeManager* pnm,
              bool enableIncremental = false);
   ~SimpSolver();
@@ -270,7 +270,7 @@ inline lbool SimpSolver::solve        (Lit p, Lit q, Lit r, bool do_simp, bool t
  }
 
  //=================================================================================================
-} /* CVC4::Minisat namespace */
-} /* CVC4 namespace */
+ }  // namespace Minisat
+ }  // namespace CVC5
 
 #endif
diff --git a/src/prop/minisat/utils/Options.h b/src/prop/minisat/utils/Options.h
index 9bddd2b23..f37b6305e 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 CVC4 {
+namespace CVC5 {
 namespace Minisat {
 
 //==================================================================================================
@@ -432,6 +432,6 @@ class BoolOption : public Option
 
 //=================================================================================================
 }
-}
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/minisat/utils/ParseUtils.h b/src/prop/minisat/utils/ParseUtils.h
index 128205967..27e454d00 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 CVC4 {
+namespace CVC5 {
 namespace Minisat {
 
 //-------------------------------------------------------------------------------------------------
@@ -120,6 +120,6 @@ static bool eagerMatch(B& in, const char* str) {
 
 //=================================================================================================
 }
-}
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index 014063f30..ab5c59dd1 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 CVC4 {
+namespace CVC5 {
 namespace prop {
 
 ProofCnfStream::ProofCnfStream(context::UserContext* u,
@@ -1012,4 +1012,4 @@ SatLiteral ProofCnfStream::handleIte(TNode node)
 }
 
 }  // namespace prop
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h
index 6f9261278..7c97a2e8e 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 CVC4 {
+namespace CVC5 {
 namespace prop {
 
 class SatProofManager;
@@ -170,6 +170,6 @@ class ProofCnfStream : public ProofGenerator
 };
 
 }  // namespace prop
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/proof_post_processor.cpp b/src/prop/proof_post_processor.cpp
index 44a30ccc6..7f075ab37 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 CVC4 {
+namespace CVC5 {
 namespace prop {
 
 ProofPostprocessCallback::ProofPostprocessCallback(
@@ -105,4 +105,4 @@ void ProofPostproccess::process(std::shared_ptr<ProofNode> pf)
 }
 
 }  // namespace prop
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/prop/proof_post_processor.h b/src/prop/proof_post_processor.h
index 9a8894eef..c74cb540f 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 CVC4 {
+namespace CVC5 {
 
 namespace prop {
 
@@ -107,6 +107,6 @@ class ProofPostproccess
 };
 
 }  // namespace prop
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 3f53433ae..9032dbb75 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 CVC4 {
+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 CVC4
+}  // namespace CVC5
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index fe5d94122..1145961a1 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 CVC4 {
+namespace CVC5 {
 
 class ResourceManager;
 class DecisionEngine;
@@ -381,6 +381,6 @@ class PropEngine
 };
 
 }  // namespace prop
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PROP_ENGINE_H */
diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp
index 399f8fd03..cb380f92d 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 CVC4 {
+namespace CVC5 {
 namespace prop {
 
 PropPfManager::PropPfManager(context::UserContext* userContext,
@@ -109,4 +109,4 @@ std::shared_ptr<ProofNode> PropPfManager::getProof()
 }
 
 }  // namespace prop
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/prop/prop_proof_manager.h b/src/prop/prop_proof_manager.h
index c429936ec..d8732c11a 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 CVC4 {
+namespace CVC5 {
 
 namespace prop {
 
@@ -92,6 +92,6 @@ class PropPfManager
 }; /* class PropPfManager */
 
 }  // namespace prop
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PROP__PROOF_MANAGER_H */
diff --git a/src/prop/registrar.h b/src/prop/registrar.h
index e54a5314b..d0fc0fe25 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 CVC4 {
+namespace CVC5 {
 namespace prop {
 
 class Registrar {
@@ -39,7 +39,7 @@ public:
 
 };/* class NullRegistrar */
 
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+}  // namespace prop
+}  // namespace CVC5
 
 #endif /* CVC4__PROP__REGISTRAR_H */
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index 6f6209a76..a11eeaa8a 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 CVC4 {
+namespace CVC5 {
 namespace prop {
 
 SatProofManager::SatProofManager(Minisat::Solver* solver,
@@ -753,4 +753,4 @@ void SatProofManager::registerSatAssumptions(const std::vector<Node>& assumps)
 }
 
 }  // namespace prop
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h
index c71e7e8a3..514f0153b 100644
--- a/src/prop/sat_proof_manager.h
+++ b/src/prop/sat_proof_manager.h
@@ -28,7 +28,7 @@ namespace Minisat {
 class Solver;
 }
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofNodeManager;
 
@@ -587,6 +587,6 @@ class SatProofManager
 }; /* class SatProofManager */
 
 }  // namespace prop
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__SAT_PROOF_MANAGER_H */
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 0cc20d2d2..f06171775 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 CVC4 {
+namespace CVC5 {
 
 namespace prop {
 
@@ -150,7 +150,7 @@ class CDCLTSatSolverInterface : public SatSolver
 
   virtual void initialize(context::Context* context,
                           prop::TheoryProxy* theoryProxy,
-                          CVC4::context::UserContext* userContext,
+                          CVC5::context::UserContext* userContext,
                           ProofNodeManager* pnm) = 0;
 
   virtual void push() = 0;
@@ -208,7 +208,7 @@ inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) {
   return out;
 }
 
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+}  // namespace prop
+}  // 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 9fbbfb60f..1d933dce8 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 CVC4 {
+namespace CVC5 {
 namespace prop {
 
 BVSatSolverInterface* SatSolverFactory::createMinisat(
@@ -76,4 +76,4 @@ SatSolver* SatSolverFactory::createKissat(StatisticsRegistry* registry,
 }
 
 }  // namespace prop
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index ca9e1ad81..97b018e09 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 CVC4 {
+namespace CVC5 {
 namespace prop {
 
 class SatSolverFactory
@@ -50,6 +50,6 @@ class SatSolverFactory
 }; /* class SatSolverFactory */
 
 }  // namespace prop
-}  // namespace CVC4
+}  // 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 3a303852a..3380329c3 100644
--- a/src/prop/sat_solver_types.cpp
+++ b/src/prop/sat_solver_types.cpp
@@ -18,11 +18,11 @@
 
 #include <algorithm>
 
-namespace CVC4 {
+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 CVC4
+}  // namespace CVC5
diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h
index a9248fdfb..392dfb2b1 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 CVC4 {
+namespace CVC5 {
 namespace prop {
 
 /**
@@ -235,4 +235,4 @@ enum SatSolverLifespan
 };
 
 }
-}
+}  // namespace CVC5
diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp
index c2a6a8462..a0819e571 100644
--- a/src/prop/skolem_def_manager.cpp
+++ b/src/prop/skolem_def_manager.cpp
@@ -16,7 +16,7 @@
 
 #include "expr/attribute.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace prop {
 
 SkolemDefManager::SkolemDefManager(context::Context* context,
@@ -170,4 +170,4 @@ void SkolemDefManager::getSkolems(
 }
 
 }  // namespace prop
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/prop/skolem_def_manager.h b/src/prop/skolem_def_manager.h
index 9bb118356..6f4ec031f 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 CVC4 {
+namespace CVC5 {
 namespace prop {
 
 /**
@@ -86,6 +86,6 @@ class SkolemDefManager
 };
 
 }  // namespace prop
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__PROP__SKOLEM_DEF_MANAGER_H */
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 66023cd88..ffec0c365 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 CVC4 {
+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 (CVC4::options::produceProofs())
+  if (CVC5::options::produceProofs())
   {
     d_propEngine->getProofCnfStream()->convertPropagation(tte);
   }
@@ -232,5 +232,5 @@ void TheoryProxy::getSkolems(TNode node,
 
 void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); }
 
-}/* CVC4::prop namespace */
-}/* CVC4 namespace */
+}  // namespace prop
+}  // namespace CVC5
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 01d98f1b9..dedd1fa49 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 CVC4 {
+namespace CVC5 {
 
 class DecisionEngine;
 class TheoryEngine;
@@ -165,8 +165,8 @@ class TheoryProxy : public Registrar
   std::unique_ptr<SkolemDefManager> d_skdm;
 }; /* class TheoryProxy */
 
-}/* CVC4::prop namespace */
+}  // namespace prop
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__PROP__SAT_H */