Rename occurrences of CVC4 to CVC5. (#6351)

This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.

38 files changed, 228 insertions, 231 deletions

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index f299459f8..536a38739 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -629,8 +629,8 @@ ApproxGLPK::ApproxGLPK(const ArithVariables& var,
 
     if (s_verbosity >= 2)
     {
-      // CVC4Message() << v  << " ";
-      // d_vars.printModel(v, CVC4Message());
+      // CVC5Message() << v  << " ";
+      // d_vars.printModel(v, CVC5Message());
     }
 
     int type;
@@ -764,8 +764,8 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{
 
     if (s_verbosity >= 2)
     {
-      CVC4Message() << v << " ";
-      d_vars.printModel(v, CVC4Message());
+      CVC5Message() << v << " ";
+      d_vars.printModel(v, CVC5Message());
     }
 
     int type;
@@ -868,9 +868,9 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{
       if(len >= rowLengthReq){
         if (s_verbosity >= 1)
         {
-          CVC4Message() << "high row " << r << " " << len << " " << avgRowLength
+          CVC5Message() << "high row " << r << " " << len << " " << avgRowLength
                         << " " << dir << endl;
-          d_vars.printModel(r, CVC4Message());
+          d_vars.printModel(r, CVC5Message());
         }
         ret.push_back(ArithRatPair(r, Rational(dir)));
       }
@@ -891,9 +891,9 @@ ArithRatPairVec ApproxGLPK::heuristicOptCoeffs() const{
       if(ubScore  >= .9 || lbScore >= .9){
         if (s_verbosity >= 1)
         {
-          CVC4Message() << "high col " << c << " " << bc << " " << ubScore
+          CVC5Message() << "high col " << c << " " << bc << " " << ubScore
                         << " " << lbScore << " " << dir << endl;
-          d_vars.printModel(c, CVC4Message());
+          d_vars.printModel(c, CVC5Message());
         }
         ret.push_back(ArithRatPair(c, Rational(c)));
       }
@@ -1016,14 +1016,14 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
       : glp_get_col_stat(prob, glpk_index);
     if (s_verbosity >= 2)
     {
-      CVC4Message() << "assignment " << vi << endl;
+      CVC5Message() << "assignment " << vi << endl;
     }
 
     bool useDefaultAssignment = false;
 
     switch(status){
     case GLP_BS:
-      // CVC4Message() << "basic" << endl;
+      // CVC5Message() << "basic" << endl;
       newBasis.add(vi);
       useDefaultAssignment = true;
       break;
@@ -1032,7 +1032,7 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
       if(!mip){
         if (s_verbosity >= 2)
         {
-          CVC4Message() << "non-basic lb" << endl;
+          CVC5Message() << "non-basic lb" << endl;
         }
         newValues.set(vi, d_vars.getLowerBound(vi));
       }else{// intentionally fall through otherwise
@@ -1043,7 +1043,7 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
       if(!mip){
         if (s_verbosity >= 2)
         {
-          CVC4Message() << "non-basic ub" << endl;
+          CVC5Message() << "non-basic ub" << endl;
         }
         newValues.set(vi, d_vars.getUpperBound(vi));
       }else {// intentionally fall through otherwise
@@ -1060,7 +1060,7 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
     if(useDefaultAssignment){
       if (s_verbosity >= 2)
       {
-        CVC4Message() << "non-basic other" << endl;
+        CVC5Message() << "non-basic other" << endl;
       }
 
       double newAssign;
@@ -1077,7 +1077,7 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
           && roughlyEqual(newAssign,
                           d_vars.getLowerBound(vi).approx(SMALL_FIXED_DELTA)))
       {
-        // CVC4Message() << "  to lb" << endl;
+        // CVC5Message() << "  to lb" << endl;
 
         newValues.set(vi, d_vars.getLowerBound(vi));
       }
@@ -1087,20 +1087,20 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
                    d_vars.getUpperBound(vi).approx(SMALL_FIXED_DELTA)))
       {
         newValues.set(vi, d_vars.getUpperBound(vi));
-        // CVC4Message() << "  to ub" << endl;
+        // CVC5Message() << "  to ub" << endl;
       }
       else
       {
         double rounded = round(newAssign);
         if (roughlyEqual(newAssign, rounded))
         {
-          // CVC4Message() << "roughly equal " << rounded << " " << newAssign <<
+          // CVC5Message() << "roughly equal " << rounded << " " << newAssign <<
           // " " << oldAssign << endl;
           newAssign = rounded;
         }
         else
         {
-          // CVC4Message() << "not roughly equal " << rounded << " " <<
+          // CVC5Message() << "not roughly equal " << rounded << " " <<
           // newAssign << " " << oldAssign << endl;
         }
 
@@ -1117,26 +1117,26 @@ ApproximateSimplex::Solution ApproxGLPK::extractSolution(bool mip) const
 
         if (roughlyEqual(newAssign, oldAssign.approx(SMALL_FIXED_DELTA)))
         {
-          // CVC4Message() << "  to prev value" << newAssign << " " << oldAssign
+          // CVC5Message() << "  to prev value" << newAssign << " " << oldAssign
           // << endl;
           proposal = d_vars.getAssignment(vi);
         }
 
         if (d_vars.strictlyLessThanLowerBound(vi, proposal))
         {
-          // CVC4Message() << "  round to lb " << d_vars.getLowerBound(vi) <<
+          // CVC5Message() << "  round to lb " << d_vars.getLowerBound(vi) <<
           // endl;
           proposal = d_vars.getLowerBound(vi);
         }
         else if (d_vars.strictlyGreaterThanUpperBound(vi, proposal))
         {
-          // CVC4Message() << "  round to ub " << d_vars.getUpperBound(vi) <<
+          // CVC5Message() << "  round to ub " << d_vars.getUpperBound(vi) <<
           // endl;
           proposal = d_vars.getUpperBound(vi);
         }
         else
         {
-          // CVC4Message() << "  use proposal" << proposal << " " << oldAssign
+          // CVC5Message() << "  use proposal" << proposal << " " << oldAssign
           // << endl;
         }
         newValues.set(vi, proposal);
diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index d74385d3b..33b0e2e26 100644
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -120,12 +120,12 @@ Result::Sat AttemptSolutionSDP::attempt(const ApproximateSimplex::Solution& sol)
     Assert(toAdd != ARITHVAR_SENTINEL);
 
     Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl;
-    // CVC4Message() << toRemove << " " << toAdd << endl;
+    // CVC5Message() << toRemove << " " << toAdd << endl;
 
     d_linEq.pivotAndUpdate(toRemove, toAdd, newValues[toRemove]);
 
     Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl;
-    // CVC4Message() << needsToBeAdded.size() << "to go" << endl;
+    // CVC5Message() << needsToBeAdded.size() << "to go" << endl;
     needsToBeAdded.remove(toAdd);
 
     bool conflict = processSignals();
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index dcd699d88..fc2506f84 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -185,7 +185,7 @@ std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v){
   return o;
 }
 
-void Constraint::debugPrint() const { CVC4Message() << *this << endl; }
+void Constraint::debugPrint() const { CVC5Message() << *this << endl; }
 
 ValueCollection::ValueCollection()
   : d_lowerBound(NullConstraint),
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 1ad23f8ca..1cd092abc 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -776,8 +776,8 @@ void DioSolver::debugPrintTrail(DioSolver::TrailIndex i) const{
   const SumPair& eq = d_trail[i].d_eq;
   const Polynomial& proof = d_trail[i].d_proof;
 
-  CVC4Message() << "d_trail[" << i << "].d_eq = " << eq.getNode() << endl;
-  CVC4Message() << "d_trail[" << i << "].d_proof = " << proof.getNode() << endl;
+  CVC5Message() << "d_trail[" << i << "].d_eq = " << eq.getNode() << endl;
+  CVC5Message() << "d_trail[" << i << "].d_proof = " << proof.getNode() << endl;
 }
 
 void DioSolver::subAndReduceCurrentFByIndex(DioSolver::SubIndex subIndex){
diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 13cc29a58..543cb9587 100644
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -104,15 +104,15 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
     {
       if (result == Result::UNSAT)
       {
-        CVC4Message() << "diff order found unsat" << endl;
+        CVC5Message() << "diff order found unsat" << endl;
       }
       else if (d_errorSet.errorEmpty())
       {
-        CVC4Message() << "diff order found model" << endl;
+        CVC5Message() << "diff order found model" << endl;
       }
       else
       {
-        CVC4Message() << "diff order missed" << endl;
+        CVC5Message() << "diff order missed" << endl;
       }
     }
   }
@@ -136,15 +136,15 @@ Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
       {
         if (result == Result::UNSAT)
         {
-          CVC4Message() << "restricted var order found unsat" << endl;
+          CVC5Message() << "restricted var order found unsat" << endl;
         }
         else if (d_errorSet.errorEmpty())
         {
-          CVC4Message() << "restricted var order found model" << endl;
+          CVC5Message() << "restricted var order found model" << endl;
         }
         else
         {
-          CVC4Message() << "restricted var order missed" << endl;
+          CVC5Message() << "restricted var order missed" << endl;
         }
       }
     }
diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index de13f4eb9..49c17172f 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -78,9 +78,9 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
   if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){
     Debug("arith::findModel") << "fcFindModel("<< instance <<") trivial" << endl;
     Assert(d_conflictVariables.empty());
-    //if (verbose)
+    // if (verbose)
     //{
-    //  CVC4Message() << "fcFindModel(" << instance << ") trivial" << endl;
+    //  CVC5Message() << "fcFindModel(" << instance << ") trivial" << endl;
     //}
     return Result::SAT;
   }
@@ -95,15 +95,15 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
     d_conflictVariables.purge();
     if (verbose)
     {
-      CVC4Message() << "fcFindModel(" << instance << ") early conflict" << endl;
+      CVC5Message() << "fcFindModel(" << instance << ") early conflict" << endl;
     }
     Debug("arith::findModel") << "fcFindModel("<< instance <<") early conflict" << endl;
     Assert(d_conflictVariables.empty());
     return Result::UNSAT;
   }else if(d_errorSet.errorEmpty()){
-    //if (verbose)
+    // if (verbose)
     //{
-    //  CVC4Message() << "fcFindModel(" << instance << ") fixed itself" << endl;
+    //  CVC5Message() << "fcFindModel(" << instance << ") fixed itself" << endl;
     //}
     Debug("arith::findModel") << "fcFindModel("<< instance <<") fixed itself" << endl;
     if (verbose) Assert(!d_errorSet.moreSignals());
@@ -133,25 +133,25 @@ Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
       ++(d_statistics.d_fcFoundUnsat);
       if (verbose)
       {
-        CVC4Message() << "fc found unsat";
+        CVC5Message() << "fc found unsat";
       }
     }else if(d_errorSet.errorEmpty()){
       ++(d_statistics.d_fcFoundSat);
       if (verbose)
       {
-        CVC4Message() << "fc found model";
+        CVC5Message() << "fc found model";
       }
     }else{
       ++(d_statistics.d_fcMissed);
       if (verbose)
       {
-        CVC4Message() << "fc missed";
+        CVC5Message() << "fc missed";
       }
     }
   }
   if (verbose)
   {
-    CVC4Message() << "(" << instance << ") pivots " << d_pivots << endl;
+    CVC5Message() << "(" << instance << ") pivots " << d_pivots << endl;
   }
 
   Assert(!d_errorSet.moreSignals());
@@ -523,7 +523,7 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit
     }
     if(degenerate(w) && selected.describesPivot()){
       ArithVar leaving = selected.leaving();
-      CVC4Message() << "degenerate " << leaving << ", atBounds "
+      CVC5Message() << "degenerate " << leaving << ", atBounds "
                     << d_linEq.basicsAtBounds(selected) << ", len "
                     << d_tableau.basicRowLength(leaving) << ", bc "
                     << d_linEq.debugBasicAtBoundCount(leaving) << endl;
@@ -574,8 +574,8 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit
 
   if (verbose)
   {
-    CVC4Message() << "conflict variable " << selected << endl;
-    CVC4Message() << ss.str();
+    CVC5Message() << "conflict variable " << selected << endl;
+    CVC5Message() << ss.str();
   }
   if(Debug.isOn("error")){ d_errorSet.debugPrint(Debug("error")); }
 
@@ -791,7 +791,7 @@ Result::Sat FCSimplexDecisionProcedure::dualLike(){
 
     if (verbose)
     {
-      debugDualLike(w, CVC4Message(), instance, prevFocusSize, prevErrorSize);
+      debugDualLike(w, CVC5Message(), instance, prevFocusSize, prevErrorSize);
     }
     Assert(debugDualLike(
         w, Debug("dualLike"), instance, prevFocusSize, prevErrorSize));
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index f9f88cddf..e1eda5d85 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -90,7 +90,7 @@ parameterized INDEXED_ROOT_PREDICATE INDEXED_ROOT_PREDICATE_OP 2 "indexed root p
 
 operator IS_INTEGER 1 "term-is-integer predicate (parameter is a real-sorted term)"
 operator TO_INTEGER 1 "convert term to integer by the floor function (parameter is a real-sorted term)"
-operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this is a no-op in CVC4, as integer is a subtype of real)"
+operator TO_REAL 1 "cast term to real (parameter is an integer-sorted term; this is a no-op in cvc5, as integer is a subtype of real)"
 
 # CAST_TO_REAL is added to distinguish between integers casted to reals internally, and
 # integers casted to reals or using the API \
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 57dbdfc82..82cc02815 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -167,12 +167,12 @@ void LinearEqualityModule::forceNewBasis(const DenseSet& newBasis){
     Assert(toAdd != ARITHVAR_SENTINEL);
 
     Trace("arith::forceNewBasis") << toRemove << " " << toAdd << endl;
-    CVC4Message() << toRemove << " " << toAdd << endl;
+    CVC5Message() << toRemove << " " << toAdd << endl;
     d_tableau.pivot(toRemove, toAdd, d_trackCallback);
     d_basicVariableUpdates(toAdd);
 
     Trace("arith::forceNewBasis") << needsToBeAdded.size() << "to go" << endl;
-    CVC4Message() << needsToBeAdded.size() << "to go" << endl;
+    CVC5Message() << needsToBeAdded.size() << "to go" << endl;
     needsToBeAdded.remove(toAdd);
   }
 }
diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h
index f8a12065f..4321800f2 100644
--- a/src/theory/arith/nl/cad/constraints.h
+++ b/src/theory/arith/nl/cad/constraints.h
@@ -75,7 +75,7 @@ class Constraints
   ConstraintVector d_constraints;
 
   /**
-   * A mapping from CVC4 variables to poly variables.
+   * A mapping from cvc5 variables to poly variables.
    */
   VariableMapper d_varMapper;
 
diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp
index 5c4391d68..b0d785b2a 100644
--- a/src/theory/arith/nl/cad/proof_generator.cpp
+++ b/src/theory/arith/nl/cad/proof_generator.cpp
@@ -69,7 +69,7 @@ std::pair<std::size_t, std::size_t> getRootIDs(
  * @param zero A node representing Rational(0)
  * @param k The index of the root (starting with 1)
  * @param poly The polynomial whose root shall be considered
- * @param vm A variable mapper from CVC4 to libpoly variables
+ * @param vm A variable mapper from cvc5 to libpoly variables
  */
 Node mkIRP(const Node& var,
            Kind rel,
diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h
index 27a711f75..b493455a6 100644
--- a/src/theory/arith/nl/cad/proof_generator.h
+++ b/src/theory/arith/nl/cad/proof_generator.h
@@ -89,7 +89,7 @@ class CADProofGenerator
    *   and the origin of this is constraint.
    *
    * @param var The variable for which the interval is excluded
-   * @param vm A variable mapper between CVC4 and libpoly variables
+   * @param vm A variable mapper between cvc5 and libpoly variables
    * @param p The polynomial of the constraint
    * @param a The current partial assignment
    * @param sc The sign condition of the constraint
@@ -113,7 +113,7 @@ class CADProofGenerator
    * @param i The concrete interval that is excluded
    * @param a The current partial assignment
    * @param s The sample point that is refuted for var
-   * @param vm A variable mapper between CVC4 and libpoly variables
+   * @param vm A variable mapper between cvc5 and libpoly variables
    */
   std::vector<Node> constructCell(Node var,
                                   const CACInterval& i,
diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp
index ed50b85cf..6e96cfe7b 100644
--- a/src/theory/arith/nl/icp/icp_solver.cpp
+++ b/src/theory/arith/nl/icp/icp_solver.cpp
@@ -371,12 +371,12 @@ void ICPSolver::check()
 
 void ICPSolver::reset(const std::vector<Node>& assertions)
 {
-  Unimplemented() << "ICPSolver requires CVC4 to be configured with LibPoly";
+  Unimplemented() << "ICPSolver requires cvc5 to be configured with LibPoly";
 }
 
 void ICPSolver::check()
 {
-  Unimplemented() << "ICPSolver requires CVC4 to be configured with LibPoly";
+  Unimplemented() << "ICPSolver requires cvc5 to be configured with LibPoly";
 }
 
 #endif /* CVC5_POLY_IMP */
diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp
index d80dacd78..e5fa31aad 100644
--- a/src/theory/arith/nl/poly_conversion.cpp
+++ b/src/theory/arith/nl/poly_conversion.cpp
@@ -218,7 +218,7 @@ struct CollectMonomialData
 {
   CollectMonomialData(VariableMapper& v) : d_vm(v) {}
 
-  /** Mapper from poly variables to CVC4 variables */
+  /** Mapper from poly variables to cvc5 variables */
   VariableMapper& d_vm;
   /** Collections of the monomial terms */
   std::vector<Node> d_terms;
diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h
index 3213df0ce..db64320d5 100644
--- a/src/theory/arith/nl/poly_conversion.h
+++ b/src/theory/arith/nl/poly_conversion.h
@@ -37,17 +37,17 @@ class BoundInference;
 
 namespace nl {
 
-/** Bijective mapping between CVC4 variables and poly variables. */
+/** Bijective mapping between cvc5 variables and poly variables. */
 struct VariableMapper
 {
-  /** A mapping from CVC4 variables to poly variables. */
+  /** A mapping from cvc5 variables to poly variables. */
   std::map<cvc5::Node, poly::Variable> mVarCVCpoly;
-  /** A mapping from poly variables to CVC4 variables. */
+  /** A mapping from poly variables to cvc5 variables. */
   std::map<poly::Variable, cvc5::Node> mVarpolyCVC;
 
   /** Retrieves the according poly variable. */
   poly::Variable operator()(const cvc5::Node& n);
-  /** Retrieves the according CVC4 variable. */
+  /** Retrieves the according cvc5 variable. */
   cvc5::Node operator()(const poly::Variable& n);
 };
 
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 1b22bc81c..fc2ed8fa9 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -97,7 +97,7 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
     d_conflictVariables.purge();
     if (verbose)
     {
-      CVC4Message() << "fcFindModel(" << instance << ") early conflict" << endl;
+      CVC5Message() << "fcFindModel(" << instance << ") early conflict" << endl;
     }
     Debug("soi::findModel") << "fcFindModel("<< instance <<") early conflict" << endl;
     Assert(d_conflictVariables.empty());
@@ -131,25 +131,25 @@ Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
       ++(d_statistics.d_soiFoundUnsat);
       if (verbose)
       {
-        CVC4Message() << "fc found unsat";
+        CVC5Message() << "fc found unsat";
       }
     }else if(d_errorSet.errorEmpty()){
       ++(d_statistics.d_soiFoundSat);
       if (verbose)
       {
-        CVC4Message() << "fc found model";
+        CVC5Message() << "fc found model";
       }
     }else{
       ++(d_statistics.d_soiMissed);
       if (verbose)
       {
-        CVC4Message() << "fc missed";
+        CVC5Message() << "fc missed";
       }
     }
   }
   if (verbose)
   {
-    CVC4Message() << "(" << instance << ") pivots " << d_pivots << endl;
+    CVC5Message() << "(" << instance << ") pivots " << d_pivots << endl;
   }
 
   Assert(!d_errorSet.moreSignals());
@@ -360,7 +360,7 @@ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, Witnes
     }
     if(degenerate(w) && selected.describesPivot()){
       ArithVar leaving = selected.leaving();
-      CVC4Message() << "degenerate " << leaving << ", atBounds "
+      CVC5Message() << "degenerate " << leaving << ", atBounds "
                     << d_linEq.basicsAtBounds(selected) << ", len "
                     << d_tableau.basicRowLength(leaving) << ", bc "
                     << d_linEq.debugBasicAtBoundCount(leaving) << endl;
@@ -411,8 +411,8 @@ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, Witnes
 
   if (verbose)
   {
-    CVC4Message() << "conflict variable " << selected << endl;
-    CVC4Message() << ss.str();
+    CVC5Message() << "conflict variable " << selected << endl;
+    CVC5Message() << ss.str();
   }
   if(Debug.isOn("error")){ d_errorSet.debugPrint(Debug("error")); }
 
@@ -971,7 +971,7 @@ Result::Sat SumOfInfeasibilitiesSPD::sumOfInfeasibilities(){
 
     if (verbose)
     {
-      debugSOI(w, CVC4Message(), instance);
+      debugSOI(w, CVC5Message(), instance);
     }
     Assert(debugSOI(w, Debug("dualLike"), instance));
   }
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index e7ff27413..4687922a0 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -3103,7 +3103,7 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
 //               mipRes = approxSolver->solveMIP(true);
 //             }
 //             d_errorSet.reduceToSignals();
-//             //CVC4Message() << "here" << endl;
+//             //CVC5Message() << "here" << endl;
 //             if(mipRes == ApproximateSimplex::ApproxSat){
 //               mipSolution = approxSolver->extractMIP();
 //               d_qflraStatus = d_attemptSolSimplex.attempt(mipSolution);
@@ -3121,7 +3121,7 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
 //           options::arithStandardCheckVarOrderPivots.set(pass2Limit);
 //           if(d_qflraStatus != Result::UNSAT){ d_qflraStatus =
 //           simplex.findModel(false); }
-//           //CVC4Message() << "done" << endl;
+//           //CVC5Message() << "done" << endl;
 //         }
 //         break;
 //       case ApproximateSimplex::ApproxUnsat:
@@ -3147,13 +3147,13 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
 //   }else{
 
 //     if(d_qflraStatus == Result::SAT_UNKNOWN){
-//       //CVC4Message() << "got sat unknown" << endl;
+//       //CVC5Message() << "got sat unknown" << endl;
 //       vector<ArithVar> toCut = cutAllBounded();
 //       if(toCut.size() > 0){
 //         //branchVector(toCut);
 //         emmittedConflictOrSplit = true;
 //       }else{
-//         //CVC4Message() << "splitting" << endl;
+//         //CVC5Message() << "splitting" << endl;
 
 //         d_qflraStatus = simplex.findModel(noPivotLimit);
 //       }
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index e2f69f19d..dffe0baf3 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -1,7 +1,7 @@
 # kinds [for builtin theory]                                          -*- sh -*-
 #
 # This "kinds" file is written in a domain-specific language for
-# declaring CVC4 kinds.  Comments are marked with #, as this line is.
+# declaring cvc5 kinds.  Comments are marked with #, as this line is.
 #
 # The first non-blank, non-comment line in this file must be a theory
 # declaration:
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index b7a62be5e..3b9b14fb7 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -74,7 +74,7 @@ class DatatypesRewriter : public TheoryRewriter
    *   Stream := cons( head : Int, tail : Stream )
    * The stream 1,0,1,0,1,0... when written in mu-notation is the term:
    *   mu x. cons( 1, mu y. cons( 0, x ) )
-   * This is represented in CVC4 by the Node:
+   * This is represented in cvc5 by the Node:
    *   cons( 1, cons( 0, c[1] ) )
    * where c[1] is a uninterpreted constant datatype with Debruijn index 1,
    * indicating that c[1] is nested underneath 1 level on the path to the
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index a62fd4894..a2306cc6a 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -633,7 +633,7 @@ symbolicProposition symbolicBitVector<isSigned>::operator>(
 }
 
 /*** Type conversion ***/
-// CVC4 nodes make no distinction between signed and unsigned, thus ...
+// cvc5 nodes make no distinction between signed and unsigned, thus ...
 template <bool isSigned>
 symbolicBitVector<true> symbolicBitVector<isSigned>::toSigned(void) const
 {
diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h
index 4225be84a..1db635cda 100644
--- a/src/theory/fp/fp_converter.h
+++ b/src/theory/fp/fp_converter.h
@@ -38,7 +38,7 @@
 #endif
 
 #ifdef CVC5_SYM_SYMBOLIC_EVAL
-// This allows debugging of the CVC4 symbolic back-end.
+// This allows debugging of the cvc5 symbolic back-end.
 // By enabling this and disabling constant folding in the rewriter,
 // SMT files that have operations on constants will be evaluated
 // during the encoding step, which means that the expressions
@@ -54,7 +54,7 @@ namespace fp {
  * This is a symfpu symbolic "back-end".  It allows the library to be used to
  * construct bit-vector expressions that compute floating-point operations.
  * This is effectively the glue between symfpu's notion of "signed bit-vector"
- * and CVC4's node.
+ * and cvc5's node.
  */
 namespace symfpuSymbolic {
 
@@ -103,7 +103,7 @@ typedef traits::bwt bwt;
 class nodeWrapper : public Node
 {
  protected:
-/* CVC5_SYM_SYMBOLIC_EVAL is for debugging CVC4 symbolic back-end issues.
+/* CVC5_SYM_SYMBOLIC_EVAL is for debugging cvc5 symbolic back-end issues.
  * Enable this and disabling constant folding will mean that operations
  * that are input with constant args are 'folded' using the symbolic encoding
  * allowing them to be traced via GDB.
@@ -255,7 +255,7 @@ class symbolicBitVector : public nodeWrapper
   symbolicProposition operator>(const symbolicBitVector<isSigned> &op) const;
 
   /*** Type conversion ***/
-  // CVC4 nodes make no distinction between signed and unsigned, thus these are
+  // cvc5 nodes make no distinction between signed and unsigned, thus these are
   // trivial
   symbolicBitVector<true> toSigned(void) const;
   symbolicBitVector<false> toUnsigned(void) const;
diff --git a/src/theory/incomplete_id.h b/src/theory/incomplete_id.h
index 1e917c942..c166d0c0a 100644
--- a/src/theory/incomplete_id.h
+++ b/src/theory/incomplete_id.h
@@ -24,7 +24,7 @@ namespace cvc5 {
 namespace theory {
 
 /**
- * Reasons for incompleteness in CVC4.
+ * Reasons for incompleteness in cvc5.
  */
 enum class IncompleteId
 {
diff --git a/src/theory/interrupted.h b/src/theory/interrupted.h
index e85917e00..bb099114d 100644
--- a/src/theory/interrupted.h
+++ b/src/theory/interrupted.h
@@ -22,7 +22,7 @@
  * Theory, the Theory should rethrow the same exception (via "throw;"
  * in the exception block) rather than return, as the Interrupted
  * instance might contain additional information needed for the
- * proper management of CVC4 components.
+ * proper management of cvc5 components.
  */
 
 #include "cvc5_private.h"
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index fa06e93a4..9d18d5145 100644
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -30,12 +30,12 @@ namespace cvc5 {
 /**
  * A LogicInfo instance describes a collection of theory modules and some
  * basic configuration about them.  Conceptually, it provides a background
- * context for all operations in CVC4.  Typically, when CVC4's SmtEngine
+ * context for all operations in cvc5.  Typically, when cvc5's SmtEngine
  * is created, it is issued a setLogic() command indicating features of the
  * assertions and queries to follow---for example, whether quantifiers are
  * used, whether integers or reals (or both) will be used, etc.
  *
- * Most places in CVC4 will only ever need to access a const reference to an
+ * Most places in cvc5 will only ever need to access a const reference to an
  * instance of this class.  Such an instance is generally set by the SmtEngine
  * when setLogic() is called.  However, mutating member functions are also
  * provided by this class so that it can be used as a more general mechanism
diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
index c27ff0fb1..baef55679 100755
--- a/src/theory/mkrewriter
+++ b/src/theory/mkrewriter
@@ -1,8 +1,8 @@
 #!/usr/bin/env bash
 #
 # mkrewriter
-# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2013  The CVC4 Project
+# Morgan Deters <mdeters@cs.nyu.edu> for cvc5
+# Copyright (c) 2010-2013  The cvc5 Project
 #
 # The purpose of this script is to create rewriter_tables.h from a template
 # and a list of theory kinds.
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index b07b1b46a..4312da406 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -1,8 +1,8 @@
 #!/usr/bin/env bash
 #
 # mktheorytraits
-# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2013  The CVC4 Project
+# Morgan Deters <mdeters@cs.nyu.edu> for cvc5
+# Copyright (c) 2010-2013  The cvc5 Project
 #
 # The purpose of this script is to create theory_traits.h from a template
 # and a list of theory kinds.
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
index 8634890b4..684751292 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -31,77 +31,78 @@ namespace inst {
 class CandidateGenerator;
 
 /** InstMatchGenerator class
-*
-* This is the default generator class for non-simple single triggers, that is,
-* triggers composed of a single term with nested term applications.
-* For example, { f( y, f( x, a ) ) } and { f( g( x ), a ) } are non-simple
-* triggers.
-*
-* Handling non-simple triggers is done by constructing a linked list of
-* InstMatchGenerator classes (see mkInstMatchGenerator), where each
-* InstMatchGenerator has a "d_next" pointer.  If d_next is NULL,
-* then this is the end of the InstMatchGenerator and the last
-* InstMatchGenerator is responsible for finalizing the instantiation.
-*
-* For (EX1), for the trigger f( y, f( x, a ) ), we construct the linked list:
-*
-* [ f( y, f( x, a ) ) ] -> [ f( x, a ) ] -> NULL
-*
-* In a call to getNextMatch,
-* if we match against a ground term f( b, c ), then the first InstMatchGenerator
-* in this list binds y to b, and tells the InstMatchGenerator [ f( x, a ) ] to
-* match f-applications in the equivalence class of c.
-*
-* CVC4 employs techniques that ensure that the number of instantiations
-* is worst-case polynomial wrt the number of ground terms.
-* Consider the axiom/pattern/context (EX2) :
-*
-*          axiom : forall x1 x2 x3 x4. F[ x1...x4 ]
-*
-*        trigger : P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )
-*
-* ground context : ~P( a, a, a, a ), a = f( c_1 ) = ... = f( c_100 )
-*
-* If E-matching were applied exhaustively, then x1, x2, x3, x4 would be
-* instantiated with all combinations of c_1, ... c_100, giving 100^4
-* instantiations.
-*
-* Instead, we enforce that at most 1 instantiation is produced for a
-* ( pattern, ground term ) pair per round. Meaning, only one instantiation is
-* generated when matching P( a, a, a, a ) against the generator
-* [P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )]. For details, see Section 3 of
-* Reynolds, Vampire 2016.
-*
-* To enforce these policies, we use a flag "d_active_add" which dictates the
-* behavior of the last element in the linked list. If d_active_add is
-*   true -> a call to getNextMatch(...) returns 1 only if adding the
-*           instantiation via a call to IMGenerator::sendInstantiation(...)
-*           successfully enqueues a lemma via a call to
-*           Instantiate::addInstantiation(...). This call may fail e.g. if we
-*           have already added the instantiation, or the instantiation is
-*           entailed.
-*   false -> a call to getNextMatch(...) returns 1 whenever an m is
-*            constructed, where typically the caller would use m.
-* This is important since a return value >0 signals that the current matched
-* terms should be flushed. Consider the above example (EX1), where
-* [ f(y,f(x,a)) ] is being matched against f(b,c),
-* [ f(x,a) ] is being matched against f(d,a) where c=f(d,a)
-* A successfully added instantiation { x->d, y->b } here signals we should
-* not produce further instantiations that match f(y,f(x,a)) with f(b,c).
-*
-* A number of special cases of triggers are covered by this generator (see
-* implementation of initialize), including :
-*   Literal triggers, e.g. x >= a, ~x = y
-*   Selector triggers, e.g. head( x )
-*   Triggers with invertible subterms, e.g. f( x+1 )
-*   Variable triggers, e.g. x
-*
-* All triggers above can be in the context of an equality, e.g.
-* { f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to
-* ground terms in the equivalence class of b.
-* { ~f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to any
-* ground terms not in the equivalence class of b.
-*/
+ *
+ * This is the default generator class for non-simple single triggers, that is,
+ * triggers composed of a single term with nested term applications.
+ * For example, { f( y, f( x, a ) ) } and { f( g( x ), a ) } are non-simple
+ * triggers.
+ *
+ * Handling non-simple triggers is done by constructing a linked list of
+ * InstMatchGenerator classes (see mkInstMatchGenerator), where each
+ * InstMatchGenerator has a "d_next" pointer.  If d_next is NULL,
+ * then this is the end of the InstMatchGenerator and the last
+ * InstMatchGenerator is responsible for finalizing the instantiation.
+ *
+ * For (EX1), for the trigger f( y, f( x, a ) ), we construct the linked list:
+ *
+ * [ f( y, f( x, a ) ) ] -> [ f( x, a ) ] -> NULL
+ *
+ * In a call to getNextMatch,
+ * if we match against a ground term f( b, c ), then the first
+ * InstMatchGenerator in this list binds y to b, and tells the
+ * InstMatchGenerator [ f( x, a ) ] to match f-applications in the equivalence
+ * class of c.
+ *
+ * cvc5 employs techniques that ensure that the number of instantiations
+ * is worst-case polynomial wrt the number of ground terms.
+ * Consider the axiom/pattern/context (EX2) :
+ *
+ *          axiom : forall x1 x2 x3 x4. F[ x1...x4 ]
+ *
+ *        trigger : P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )
+ *
+ * ground context : ~P( a, a, a, a ), a = f( c_1 ) = ... = f( c_100 )
+ *
+ * If E-matching were applied exhaustively, then x1, x2, x3, x4 would be
+ * instantiated with all combinations of c_1, ... c_100, giving 100^4
+ * instantiations.
+ *
+ * Instead, we enforce that at most 1 instantiation is produced for a
+ * ( pattern, ground term ) pair per round. Meaning, only one instantiation is
+ * generated when matching P( a, a, a, a ) against the generator
+ * [P( f( x1 ), f( x2 ), f( x3 ), f( x4 ) )]. For details, see Section 3 of
+ * Reynolds, Vampire 2016.
+ *
+ * To enforce these policies, we use a flag "d_active_add" which dictates the
+ * behavior of the last element in the linked list. If d_active_add is
+ *   true -> a call to getNextMatch(...) returns 1 only if adding the
+ *           instantiation via a call to IMGenerator::sendInstantiation(...)
+ *           successfully enqueues a lemma via a call to
+ *           Instantiate::addInstantiation(...). This call may fail e.g. if we
+ *           have already added the instantiation, or the instantiation is
+ *           entailed.
+ *   false -> a call to getNextMatch(...) returns 1 whenever an m is
+ *            constructed, where typically the caller would use m.
+ * This is important since a return value >0 signals that the current matched
+ * terms should be flushed. Consider the above example (EX1), where
+ * [ f(y,f(x,a)) ] is being matched against f(b,c),
+ * [ f(x,a) ] is being matched against f(d,a) where c=f(d,a)
+ * A successfully added instantiation { x->d, y->b } here signals we should
+ * not produce further instantiations that match f(y,f(x,a)) with f(b,c).
+ *
+ * A number of special cases of triggers are covered by this generator (see
+ * implementation of initialize), including :
+ *   Literal triggers, e.g. x >= a, ~x = y
+ *   Selector triggers, e.g. head( x )
+ *   Triggers with invertible subterms, e.g. f( x+1 )
+ *   Variable triggers, e.g. x
+ *
+ * All triggers above can be in the context of an equality, e.g.
+ * { f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to
+ * ground terms in the equivalence class of b.
+ * { ~f( y, f( x, a ) ) = b } is a trigger that matches f( y, f( x, a ) ) to any
+ * ground terms not in the equivalence class of b.
+ */
 class InstMatchGenerator : public IMGenerator {
  public:
   /** destructor */
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
index e15d476a3..afe43a604 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
@@ -37,7 +37,7 @@ namespace inst {
  * InstMatchGeneratorMultiLinear at the head and a list of trailing
  * InstMatchGenerators.
  *
- * CVC4 employs techniques that ensure that the number of instantiations
+ * cvc5 employs techniques that ensure that the number of instantiations
  * is worst-case polynomial wrt the number of ground terms, where this class
  * lifts this policy to multi-triggers. In particular consider
  *
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index dbfae5382..172e93c12 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -39,66 +39,62 @@ namespace inst {
 class IMGenerator;
 class InstMatchGenerator;
 /** A collection of nodes representing a trigger.
-*
-* This class encapsulates all implementations of E-matching in CVC4.
-* Its primary use is as a utility of the quantifiers module InstantiationEngine
-* (see theory/quantifiers/ematching/instantiation_engine.h) which uses Trigger to make
-* appropriate calls to Instantiate::addInstantiation(...)
-* (see theory/instantiate.h) for the instantiate utility of the quantifiers
-* engine (d_quantEngine) associated with this trigger.  These calls
-* queue instantiation lemmas to the output channel of TheoryQuantifiers during
-* a full effort check.
-*
-* Concretely, a Trigger* t is used in the following way during a full effort
-* check. Assume that t is associated with quantified formula q (see field d_f).
-* We call :
-*
-* // setup initial information
-* t->resetInstantiationRound();
-* // will produce instantiations based on matching with all terms
-* t->reset( Node::null() );
-* // add all instantiations based on E-matching with this trigger and the
-* // current context
-* t->addInstantiations();
-*
-* This will result in (a set of) calls to
-* Instantiate::addInstantiation(q, m1)...Instantiate::addInstantiation(q, mn),
-* where m1...mn are InstMatch objects. These calls add the corresponding
-* instantiation lemma for (q,mi) on the output channel associated with
-* d_quantEngine.
-*
-* The Trigger class is wrapper around an underlying IMGenerator class, which
-* implements various forms of E-matching for its set of nodes (d_nodes), which
-* is refered to in the literature as a "trigger". A trigger is a set of terms
-* whose free variables are the bound variables of a quantified formula q,
-* and that is used to guide instantiations for q (for example, see "Efficient
-* E-Matching for SMT Solvers" by de Moura et al).
-*
-* For example of an instantiation lemma produced by E-matching :
-*
-* quantified formula : forall x. P( x )
-*            trigger : P( x )
-*     ground context : ~P( a )
-*
-* Then E-matching matches P( x ) and P( a ), resulting in the match { x -> a }
-* which is used to generate the instantiation lemma :
-*   (forall x. P( x )) => P( a )
-*
-* Terms that are provided as input to a Trigger class via mkTrigger
-* should be in "instantiation constant form", see TermUtil::getInstConstantNode.
-* Say we have quantified formula q whose AST is the Node
-*   (FORALL
-*     (BOUND_VAR_LIST x)
-*     (NOT (P x))
-*     (INST_PATTERN_LIST (INST_PATTERN (P x))))
-* then TermUtil::getInstConstantNode( q, (P x) ) = (P IC) where
-* IC = TermUtil::getInstantiationConstant( q, i ).
-* Trigger expects as input (P IC) to represent the Trigger (P x). This form
-* ensures that references to bound variables are unique to quantified formulas,
-* which is required to ensure the correctness of instantiation lemmas we
-* generate.
-*
-*/
+ *
+ * This class encapsulates all implementations of E-matching in cvc5.
+ * Its primary use is as a utility of the quantifiers module InstantiationEngine
+ * (see theory/quantifiers/ematching/instantiation_engine.h) which uses Trigger
+ * to make appropriate calls to Instantiate::addInstantiation(...) (see
+ * theory/instantiate.h) for the instantiate utility of the quantifiers engine
+ * (d_quantEngine) associated with this trigger.  These calls queue
+ * instantiation lemmas to the output channel of TheoryQuantifiers during a full
+ * effort check.
+ *
+ * Concretely, a Trigger* t is used in the following way during a full effort
+ * check. Assume that t is associated with quantified formula q (see field d_f).
+ * We call :
+ *
+ * // setup initial information
+ * t->resetInstantiationRound();
+ * // will produce instantiations based on matching with all terms
+ * t->reset( Node::null() );
+ * // add all instantiations based on E-matching with this trigger and the
+ * // current context
+ * t->addInstantiations();
+ *
+ * This will result in (a set of) calls to
+ * Instantiate::addInstantiation(q, m1)...Instantiate::addInstantiation(q, mn),
+ * where m1...mn are InstMatch objects. These calls add the corresponding
+ * instantiation lemma for (q,mi) on the output channel associated with
+ * d_quantEngine.
+ *
+ * The Trigger class is wrapper around an underlying IMGenerator class, which
+ * implements various forms of E-matching for its set of nodes (d_nodes), which
+ * is refered to in the literature as a "trigger". A trigger is a set of terms
+ * whose free variables are the bound variables of a quantified formula q,
+ * and that is used to guide instantiations for q (for example, see "Efficient
+ * E-Matching for SMT Solvers" by de Moura et al).
+ *
+ * For example of an instantiation lemma produced by E-matching :
+ *
+ * quantified formula : forall x. P( x )
+ *            trigger : P( x )
+ *     ground context : ~P( a )
+ *
+ * Then E-matching matches P( x ) and P( a ), resulting in the match { x -> a }
+ * which is used to generate the instantiation lemma :
+ *   (forall x. P( x )) => P( a )
+ *
+ * Terms that are provided as input to a Trigger class via mkTrigger
+ * should be in "instantiation constant form", see
+ * TermUtil::getInstConstantNode. Say we have quantified formula q whose AST is
+ * the Node (FORALL (BOUND_VAR_LIST x) (NOT (P x)) (INST_PATTERN_LIST
+ * (INST_PATTERN (P x)))) then TermUtil::getInstConstantNode( q, (P x) ) = (P
+ * IC) where IC = TermUtil::getInstantiationConstant( q, i ). Trigger expects as
+ * input (P IC) to represent the Trigger (P x). This form ensures that
+ * references to bound variables are unique to quantified formulas, which is
+ * required to ensure the correctness of instantiation lemmas we generate.
+ *
+ */
 class Trigger {
   friend class IMGenerator;
 
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 4545b2d39..841cd4ab9 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -675,7 +675,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
           Node ev = d_quant_models[f].evaluate(fmfmc, inst);
           if (ev == d_true)
           {
-            CVC4Message() << "WARNING: instantiation was true! " << f << " "
+            CVC5Message() << "WARNING: instantiation was true! " << f << " "
                           << mcond[i] << std::endl;
             AlwaysAssert(false);
           }
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 585032dc4..5eba46657 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -104,7 +104,7 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e)
 
     if( addedLemmas==0 ){
       Trace("model-engine-debug") << "No lemmas added, incomplete = " << ( d_incomplete_check || !d_incomplete_quants.empty() ) << std::endl;
-      //CVC4 will answer SAT or unknown
+      // cvc5 will answer SAT or unknown
       if( Trace.isOn("fmf-consistent") ){
         Trace("fmf-consistent") << std::endl;
         debugPrint("fmf-consistent");
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index f89bdf1f2..1abbd1989 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -173,7 +173,7 @@ void QuantAttributes::computeAttributes( Node q ) {
   {
     Node f = qa.d_fundef_f;
     if( d_fun_defs.find( f )!=d_fun_defs.end() ){
-      CVC4Message() << "Cannot define function " << f << " more than once."
+      CVC5Message() << "Cannot define function " << f << " more than once."
                     << std::endl;
       AlwaysAssert(false);
     }
diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp
index 7597054d9..3c3dd8d84 100644
--- a/src/theory/quantifiers/query_generator.cpp
+++ b/src/theory/quantifiers/query_generator.cpp
@@ -166,7 +166,7 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
     if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
     {
       std::stringstream ss;
-      ss << "--sygus-rr-query-gen detected unsoundness in CVC4 on input " << qy
+      ss << "--sygus-rr-query-gen detected unsoundness in cvc5 on input " << qy
          << "!" << std::endl;
       ss << "This query has a model : " << std::endl;
       std::vector<Node> pt;
@@ -176,7 +176,7 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
       {
         ss << "  " << d_vars[i] << " -> " << pt[i] << std::endl;
       }
-      ss << "but CVC4 answered unsat!" << std::endl;
+      ss << "but cvc5 answered unsat!" << std::endl;
       AlwaysAssert(false) << ss.str();
     }
     if (options::sygusQueryGenDumpFiles()
diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp
index 2f21a50e1..431156c03 100644
--- a/src/theory/quantifiers/term_tuple_enumerator.cpp
+++ b/src/theory/quantifiers/term_tuple_enumerator.cpp
@@ -36,7 +36,7 @@
 namespace cvc5 {
 
 template <typename T>
-static CVC4ostream& operator<<(CVC4ostream& out, const std::vector<T>& v)
+static CVC5ostream& operator<<(CVC5ostream& out, const std::vector<T>& v)
 {
   out << "[ ";
   std::copy(v.begin(), v.end(), std::ostream_iterator<T>(out, " "));
diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds
index 564779f6a..0f15727e0 100644
--- a/src/theory/sets/kinds
+++ b/src/theory/sets/kinds
@@ -63,7 +63,7 @@ nullaryoperator UNIVERSE_SET "(finite) universe set, all set variables must be i
 # forall y. ( exists x1...xn. P[x1...xn] ^ t[x1...xn] = y ) <=> (member y C)
 # where y ranges over the element type of the (set) type of the comprehension.
 # Notice that since all sets must be interpreted as finite, this means that
-# CVC4 will not be able to construct a model for any set comprehension such
+# cvc5 will not be able to construct a model for any set comprehension such
 # that there are infinitely many y that satisfy the left hand side of the
 # equivalence above. The same limitation occurs more generally when combining
 # finite sets with quantified formulas.
diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index 76edde5ae..2ca8696b0 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -51,7 +51,7 @@ public:
  * This class implements inference schemes described in Meng et al. CADE 2017
  * for handling quantifier-free constraints in the theory of relations.
  *
- * In CVC4, relations are represented as sets of tuples. The theory of
+ * In cvc5, relations are represented as sets of tuples. The theory of
  * relations includes constraints over operators, e.g. TRANSPOSE, JOIN and so
  * on, which apply to sets of tuples.
  *
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 4148f51b3..5c4b36043 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -214,7 +214,7 @@ void SubstitutionMap::print(ostream& out) const {
   }
 }
 
-void SubstitutionMap::debugPrint() const { print(CVC4Message.getStream()); }
+void SubstitutionMap::debugPrint() const { print(CVC5Message.getStream()); }
 
 }  // namespace theory
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 3eacdaa20..e870860c5 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -94,7 +94,7 @@ class PropEngine;
  * This is essentially an abstraction for a collection of theories.  A
  * TheoryEngine provides services to a PropEngine, making various
  * T-solvers look like a single unit to the propositional part of
- * CVC4.
+ * cvc5.
  */
 class TheoryEngine {
 
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 25f87de2c..166df3c80 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1023,7 +1023,7 @@ int SortModel::addSplit(Region* r)
       }
       if (ss == b_t)
       {
-        CVC4Message() << "Bad split " << s << std::endl;
+        CVC5Message() << "Bad split " << s << std::endl;
         AlwaysAssert(false);
       }
     }
@@ -1420,7 +1420,7 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
           for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
             if( !it->second->hasCardinalityAsserted() ){
               Trace("uf-ss-warn") << "WARNING: Assert " << n << " as a decision before cardinality for " << it->first << "." << std::endl;
-              // CVC4Message() << "Error: constraint asserted before cardinality
+              // CVC5Message() << "Error: constraint asserted before cardinality
               // for " << it->first << std::endl; Unimplemented();
             }
           }