Rename CVC4__ header guards to CVC5__. (#6326)

37 files changed, 93 insertions, 93 deletions

diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index 338f54da2..0d5d4ce74 100644
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__NL__CAD__CDCAC_H
-#define CVC4__THEORY__ARITH__NL__CAD__CDCAC_H
+#ifndef CVC5__THEORY__ARITH__NL__CAD__CDCAC_H
+#define CVC5__THEORY__ARITH__NL__CAD__CDCAC_H
 
 #ifdef CVC4_POLY_IMP
 
diff --git a/src/theory/arith/nl/cad/cdcac_utils.h b/src/theory/arith/nl/cad/cdcac_utils.h
index 607a2226f..3cfbb138c 100644
--- a/src/theory/arith/nl/cad/cdcac_utils.h
+++ b/src/theory/arith/nl/cad/cdcac_utils.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H
-#define CVC4__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H
+#ifndef CVC5__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H
+#define CVC5__THEORY__ARITH__NL__CAD__CDCAC_UTILS_H
 
 #ifdef CVC4_POLY_IMP
 
diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h
index e9e59c40b..efc69d468 100644
--- a/src/theory/arith/nl/cad/constraints.h
+++ b/src/theory/arith/nl/cad/constraints.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__NL__CAD__CONSTRAINTS_H
-#define CVC4__THEORY__ARITH__NL__CAD__CONSTRAINTS_H
+#ifndef CVC5__THEORY__ARITH__NL__CAD__CONSTRAINTS_H
+#define CVC5__THEORY__ARITH__NL__CAD__CONSTRAINTS_H
 
 #ifdef CVC4_POLY_IMP
 
diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h
index 94bdfc3ef..c1ce91303 100644
--- a/src/theory/arith/nl/cad/projections.h
+++ b/src/theory/arith/nl/cad/projections.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__NL__CAD_PROJECTIONS_H
-#define CVC4__THEORY__ARITH__NL__CAD_PROJECTIONS_H
+#ifndef CVC5__THEORY__ARITH__NL__CAD_PROJECTIONS_H
+#define CVC5__THEORY__ARITH__NL__CAD_PROJECTIONS_H
 
 #ifdef CVC4_USE_POLY
 
diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h
index 9100762b7..d2013e14b 100644
--- a/src/theory/arith/nl/cad/proof_checker.h
+++ b/src/theory/arith/nl/cad/proof_checker.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H
-#define CVC4__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H
+#define CVC5__THEORY__ARITH__NL__CAD__PROOF_CHECKER_H
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
@@ -55,4 +55,4 @@ class CADProofRuleChecker : public ProofRuleChecker
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__STRINGS__PROOF_CHECKER_H */
diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h
index 76a72f9c5..9365cc337 100644
--- a/src/theory/arith/nl/cad/proof_generator.h
+++ b/src/theory/arith/nl/cad/proof_generator.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
-#define CVC4__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
+#ifndef CVC5__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
+#define CVC5__THEORY__ARITH__NL__CAD__PROOF_GENERATOR_H
 
 #ifdef CVC4_POLY_IMP
 
diff --git a/src/theory/arith/nl/cad/variable_ordering.h b/src/theory/arith/nl/cad/variable_ordering.h
index 0ab585197..b4336d395 100644
--- a/src/theory/arith/nl/cad/variable_ordering.h
+++ b/src/theory/arith/nl/cad/variable_ordering.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H
-#define CVC4__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H
+#ifndef CVC5__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H
+#define CVC5__THEORY__ARITH__NL__CAD__VARIABLE_ORDERING_H
 
 #ifdef CVC4_POLY_IMP
 
diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h
index 620679735..2ea27fce7 100644
--- a/src/theory/arith/nl/cad_solver.h
+++ b/src/theory/arith/nl/cad_solver.h
@@ -12,8 +12,8 @@
  ** \brief CAD-based solver based on https://arxiv.org/pdf/2003.05633.pdf.
  **/
 
-#ifndef CVC4__THEORY__ARITH__CAD_SOLVER_H
-#define CVC4__THEORY__ARITH__CAD_SOLVER_H
+#ifndef CVC5__THEORY__ARITH__CAD_SOLVER_H
+#define CVC5__THEORY__ARITH__CAD_SOLVER_H
 
 #include <vector>
 
@@ -112,4 +112,4 @@ class CadSolver
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__CAD_SOLVER_H */
+#endif /* CVC5__THEORY__ARITH__CAD_SOLVER_H */
diff --git a/src/theory/arith/nl/ext/constraint.h b/src/theory/arith/nl/ext/constraint.h
index a96949a1e..ef9f8fef3 100644
--- a/src/theory/arith/nl/ext/constraint.h
+++ b/src/theory/arith/nl/ext/constraint.h
@@ -12,8 +12,8 @@
  ** \brief Utilities for non-linear constraints
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__EXT__CONSTRAINT_H
-#define CVC4__THEORY__ARITH__NL__EXT__CONSTRAINT_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__CONSTRAINT_H
+#define CVC5__THEORY__ARITH__NL__EXT__CONSTRAINT_H
 
 #include <map>
 #include <vector>
@@ -86,4 +86,4 @@ class ConstraintDb
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__NL_SOLVER_H */
+#endif /* CVC5__THEORY__ARITH__NL_SOLVER_H */
diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h
index 2d20e1557..1571f3173 100644
--- a/src/theory/arith/nl/ext/ext_state.h
+++ b/src/theory/arith/nl/ext/ext_state.h
@@ -12,8 +12,8 @@
  ** \brief Common data shared by multiple checks
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__EXT__SHARED_CHECK_DATA_H
-#define CVC4__THEORY__ARITH__NL__EXT__SHARED_CHECK_DATA_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__SHARED_CHECK_DATA_H
+#define CVC5__THEORY__ARITH__NL__EXT__SHARED_CHECK_DATA_H
 
 #include <vector>
 
diff --git a/src/theory/arith/nl/ext/factoring_check.h b/src/theory/arith/nl/ext/factoring_check.h
index 08154cb98..feff91112 100644
--- a/src/theory/arith/nl/ext/factoring_check.h
+++ b/src/theory/arith/nl/ext/factoring_check.h
@@ -12,8 +12,8 @@
  ** \brief Check for factoring lemma
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__EXT__FACTORING_CHECK_H
-#define CVC4__THEORY__ARITH__NL__EXT__FACTORING_CHECK_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__FACTORING_CHECK_H
+#define CVC5__THEORY__ARITH__NL__EXT__FACTORING_CHECK_H
 
 #include <vector>
 
diff --git a/src/theory/arith/nl/ext/monomial.h b/src/theory/arith/nl/ext/monomial.h
index 6646e4a73..bbae33eda 100644
--- a/src/theory/arith/nl/ext/monomial.h
+++ b/src/theory/arith/nl/ext/monomial.h
@@ -12,8 +12,8 @@
  ** \brief Utilities for monomials
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_H
-#define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_H
+#define CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_H
 
 #include <map>
 #include <vector>
@@ -146,4 +146,4 @@ class MonomialDb
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__NL_MONOMIAL_H */
+#endif /* CVC5__THEORY__ARITH__NL_MONOMIAL_H */
diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.h b/src/theory/arith/nl/ext/monomial_bounds_check.h
index a19c61e64..e95cda778 100644
--- a/src/theory/arith/nl/ext/monomial_bounds_check.h
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.h
@@ -12,8 +12,8 @@
  ** \brief Check for monomial bound inference lemmas
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_BOUNDS_CHECK_H
-#define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_BOUNDS_CHECK_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_BOUNDS_CHECK_H
+#define CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_BOUNDS_CHECK_H
 
 #include "expr/node.h"
 #include "theory/arith/nl/ext/constraint.h"
diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h
index f242182b4..f84d69b6b 100644
--- a/src/theory/arith/nl/ext/monomial_check.h
+++ b/src/theory/arith/nl/ext/monomial_check.h
@@ -12,8 +12,8 @@
  ** \brief Check for some monomial lemmas
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
-#define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
+#define CVC5__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H
 
 #include "expr/node.h"
 #include "theory/arith/nl/ext/monomial.h"
diff --git a/src/theory/arith/nl/ext/proof_checker.h b/src/theory/arith/nl/ext/proof_checker.h
index 90518fc08..5e901ddf5 100644
--- a/src/theory/arith/nl/ext/proof_checker.h
+++ b/src/theory/arith/nl/ext/proof_checker.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H
-#define CVC4__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H
+#define CVC5__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
@@ -53,4 +53,4 @@ class ExtProofRuleChecker : public ProofRuleChecker
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__STRINGS__PROOF_CHECKER_H */
diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h
index 04148bd19..bd07a79f6 100644
--- a/src/theory/arith/nl/ext/split_zero_check.h
+++ b/src/theory/arith/nl/ext/split_zero_check.h
@@ -12,8 +12,8 @@
  ** \brief Check for split zero lemma
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H
-#define CVC4__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H
+#define CVC5__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H
 
 #include "expr/node.h"
 #include "context/cdhashset.h"
diff --git a/src/theory/arith/nl/ext/tangent_plane_check.h b/src/theory/arith/nl/ext/tangent_plane_check.h
index b5159e721..b5fd797aa 100644
--- a/src/theory/arith/nl/ext/tangent_plane_check.h
+++ b/src/theory/arith/nl/ext/tangent_plane_check.h
@@ -12,8 +12,8 @@
  ** \brief Check for tangent_plane lemma
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H
-#define CVC4__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H
+#define CVC5__THEORY__ARITH__NL__EXT__TANGENT_PLANE_CHECK_H
 
 #include <map>
 
diff --git a/src/theory/arith/nl/ext_theory_callback.h b/src/theory/arith/nl/ext_theory_callback.h
index 78ea3b2b6..56faacddd 100644
--- a/src/theory/arith/nl/ext_theory_callback.h
+++ b/src/theory/arith/nl/ext_theory_callback.h
@@ -12,8 +12,8 @@
  ** \brief The extended theory callback for non-linear arithmetic
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H
-#define CVC4__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H
+#ifndef CVC5__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H
+#define CVC5__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H
 
 #include "expr/node.h"
 #include "theory/ext_theory.h"
@@ -87,4 +87,4 @@ class NlExtTheoryCallback : public ExtTheoryCallback
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H */
+#endif /* CVC5__THEORY__ARITH__NL__EXT_THEORY_CALLBACK_H */
diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
index 2b7f90e9b..52f97bf0e 100644
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -12,8 +12,8 @@
  ** \brief Solver for integer and (IAND) constraints
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__IAND_SOLVER_H
-#define CVC4__THEORY__ARITH__NL__IAND_SOLVER_H
+#ifndef CVC5__THEORY__ARITH__NL__IAND_SOLVER_H
+#define CVC5__THEORY__ARITH__NL__IAND_SOLVER_H
 
 #include <map>
 #include <vector>
@@ -134,4 +134,4 @@ class IAndSolver
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__IAND_SOLVER_H */
+#endif /* CVC5__THEORY__ARITH__IAND_SOLVER_H */
diff --git a/src/theory/arith/nl/iand_utils.h b/src/theory/arith/nl/iand_utils.h
index 60c3cbe13..cad5c80d5 100644
--- a/src/theory/arith/nl/iand_utils.h
+++ b/src/theory/arith/nl/iand_utils.h
@@ -13,8 +13,8 @@
  ** the value of iand.
  **/
 
-#ifndef CVC4__THEORY__ARITH__IAND_TABLE_H
-#define CVC4__THEORY__ARITH__IAND_TABLE_H
+#ifndef CVC5__THEORY__ARITH__IAND_TABLE_H
+#define CVC5__THEORY__ARITH__IAND_TABLE_H
 
 #include <map>
 
@@ -171,4 +171,4 @@ class IAndUtils
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__IAND_TABLE_H */
+#endif /* CVC5__THEORY__ARITH__IAND_TABLE_H */
diff --git a/src/theory/arith/nl/icp/candidate.h b/src/theory/arith/nl/icp/candidate.h
index 4bcbf3e85..524342658 100644
--- a/src/theory/arith/nl/icp/candidate.h
+++ b/src/theory/arith/nl/icp/candidate.h
@@ -12,8 +12,8 @@
  ** \brief Represents a contraction candidate for ICP-style propagation.
  **/
 
-#ifndef CVC4__THEORY__ARITH__ICP__CANDIDATE_H
-#define CVC4__THEORY__ARITH__ICP__CANDIDATE_H
+#ifndef CVC5__THEORY__ARITH__ICP__CANDIDATE_H
+#define CVC5__THEORY__ARITH__ICP__CANDIDATE_H
 
 #include "cvc4_private.h"
 
diff --git a/src/theory/arith/nl/icp/contraction_origins.h b/src/theory/arith/nl/icp/contraction_origins.h
index dfddbce78..fd899cfd2 100644
--- a/src/theory/arith/nl/icp/contraction_origins.h
+++ b/src/theory/arith/nl/icp/contraction_origins.h
@@ -12,8 +12,8 @@
  ** \brief Implements a way to track the origins of ICP-style contractions.
  **/
 
-#ifndef CVC4__THEORY__ARITH__ICP__CONTRACTION_ORIGINS_H
-#define CVC4__THEORY__ARITH__ICP__CONTRACTION_ORIGINS_H
+#ifndef CVC5__THEORY__ARITH__ICP__CONTRACTION_ORIGINS_H
+#define CVC5__THEORY__ARITH__ICP__CONTRACTION_ORIGINS_H
 
 #include <memory>
 #include <vector>
diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h
index 11fd9ac1b..b392dc430 100644
--- a/src/theory/arith/nl/icp/icp_solver.h
+++ b/src/theory/arith/nl/icp/icp_solver.h
@@ -12,8 +12,8 @@
  ** \brief Implements a ICP-based solver for nonlinear arithmetic.
  **/
 
-#ifndef CVC4__THEORY__ARITH__ICP__ICP_SOLVER_H
-#define CVC4__THEORY__ARITH__ICP__ICP_SOLVER_H
+#ifndef CVC5__THEORY__ARITH__ICP__ICP_SOLVER_H
+#define CVC5__THEORY__ARITH__ICP__ICP_SOLVER_H
 
 #include "cvc4_private.h"
 
diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h
index dd4afadfc..a77a605d0 100644
--- a/src/theory/arith/nl/icp/intersection.h
+++ b/src/theory/arith/nl/icp/intersection.h
@@ -12,8 +12,8 @@
  ** \brief Implement intersection of intervals for propagation.
  **/
 
-#ifndef CVC4__THEORY__ARITH__ICP__INTERSECTION_H
-#define CVC4__THEORY__ARITH__ICP__INTERSECTION_H
+#ifndef CVC5__THEORY__ARITH__ICP__INTERSECTION_H
+#define CVC5__THEORY__ARITH__ICP__INTERSECTION_H
 
 #include "cvc4_private.h"
 
diff --git a/src/theory/arith/nl/icp/interval.h b/src/theory/arith/nl/icp/interval.h
index 981355e4a..7716d029f 100644
--- a/src/theory/arith/nl/icp/interval.h
+++ b/src/theory/arith/nl/icp/interval.h
@@ -12,8 +12,8 @@
  ** \brief
  **/
 
-#ifndef CVC4__THEORY__ARITH__ICP__INTERVAL_H
-#define CVC4__THEORY__ARITH__ICP__INTERVAL_H
+#ifndef CVC5__THEORY__ARITH__ICP__INTERVAL_H
+#define CVC5__THEORY__ARITH__ICP__INTERVAL_H
 
 #include "cvc4_private.h"
 
diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h
index 32fe763b4..474212821 100644
--- a/src/theory/arith/nl/nl_lemma_utils.h
+++ b/src/theory/arith/nl/nl_lemma_utils.h
@@ -12,8 +12,8 @@
  ** \brief Utilities for processing lemmas from the non-linear solver
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__NL_LEMMA_UTILS_H
-#define CVC4__THEORY__ARITH__NL__NL_LEMMA_UTILS_H
+#ifndef CVC5__THEORY__ARITH__NL__NL_LEMMA_UTILS_H
+#define CVC5__THEORY__ARITH__NL__NL_LEMMA_UTILS_H
 
 #include <tuple>
 #include <vector>
@@ -146,4 +146,4 @@ class ArgTrie
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__NL_LEMMA_UTILS_H */
+#endif /* CVC5__THEORY__ARITH__NL_LEMMA_UTILS_H */
diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h
index 9da8738b6..4a50cd54f 100644
--- a/src/theory/arith/nl/nl_model.h
+++ b/src/theory/arith/nl/nl_model.h
@@ -12,8 +12,8 @@
  ** \brief Model object for the non-linear extension class
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__NL_MODEL_H
-#define CVC4__THEORY__ARITH__NL__NL_MODEL_H
+#ifndef CVC5__THEORY__ARITH__NL__NL_MODEL_H
+#define CVC5__THEORY__ARITH__NL__NL_MODEL_H
 
 #include <map>
 #include <unordered_map>
@@ -331,4 +331,4 @@ class NlModel
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */
+#endif /* CVC5__THEORY__ARITH__NONLINEAR_EXTENSION_H */
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 722741d7d..5dd1374cd 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -15,8 +15,8 @@
  ** multiplication via axiom instantiations.
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H
-#define CVC4__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H
+#ifndef CVC5__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H
+#define CVC5__THEORY__ARITH__NL__NONLINEAR_EXTENSION_H
 
 #include <map>
 #include <vector>
@@ -298,4 +298,4 @@ class NonlinearExtension
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */
+#endif /* CVC5__THEORY__ARITH__NONLINEAR_EXTENSION_H */
diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h
index 9aef0db18..0a9d0f313 100644
--- a/src/theory/arith/nl/poly_conversion.h
+++ b/src/theory/arith/nl/poly_conversion.h
@@ -14,8 +14,8 @@
  ** Utilities for converting to and from LibPoly objects.
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__POLY_CONVERSION_H
-#define CVC4__THEORY__ARITH__NL__POLY_CONVERSION_H
+#ifndef CVC5__THEORY__ARITH__NL__POLY_CONVERSION_H
+#define CVC5__THEORY__ARITH__NL__POLY_CONVERSION_H
 
 #include "cvc4_private.h"
 
diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h
index 66f41375b..3e947160e 100644
--- a/src/theory/arith/nl/stats.h
+++ b/src/theory/arith/nl/stats.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__NL__STATS_H
-#define CVC4__THEORY__ARITH__NL__STATS_H
+#ifndef CVC5__THEORY__ARITH__NL__STATS_H
+#define CVC5__THEORY__ARITH__NL__STATS_H
 
 #include "util/statistics_registry.h"
 
@@ -46,4 +46,4 @@ class NlStats
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__NL__STATS_H */
+#endif /* CVC5__THEORY__ARITH__NL__STATS_H */
diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h
index 139db7459..4fc115476 100644
--- a/src/theory/arith/nl/strategy.h
+++ b/src/theory/arith/nl/strategy.h
@@ -12,8 +12,8 @@
  ** \brief Strategies for the nonlinear extension
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__STRATEGY_H
-#define CVC4__THEORY__ARITH__NL__STRATEGY_H
+#ifndef CVC5__THEORY__ARITH__NL__STRATEGY_H
+#define CVC5__THEORY__ARITH__NL__STRATEGY_H
 
 #include <iosfwd>
 #include <vector>
@@ -175,4 +175,4 @@ class Strategy
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__NL__STRATEGY_H */
+#endif /* CVC5__THEORY__ARITH__NL__STRATEGY_H */
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h
index c5eb45728..a7ae92498 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.h
+++ b/src/theory/arith/nl/transcendental/exponential_solver.h
@@ -12,8 +12,8 @@
  ** \brief Solving for handling exponential function.
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H
-#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H
+#ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H
+#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__EXPONENTIAL_SOLVER_H
 
 #include <map>
 
@@ -110,4 +110,4 @@ class ExponentialSolver
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
+#endif /* CVC5__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
diff --git a/src/theory/arith/nl/transcendental/proof_checker.h b/src/theory/arith/nl/transcendental/proof_checker.h
index a4c8b55cb..83788b60e 100644
--- a/src/theory/arith/nl/transcendental/proof_checker.h
+++ b/src/theory/arith/nl/transcendental/proof_checker.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__PROOF_CHECKER_H
-#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__PROOF_CHECKER_H
+#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__PROOF_CHECKER_H
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
@@ -55,4 +55,4 @@ class TranscendentalProofRuleChecker : public ProofRuleChecker
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__STRINGS__PROOF_CHECKER_H */
diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h
index b85d0dc48..80b4fb10b 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.h
+++ b/src/theory/arith/nl/transcendental/sine_solver.h
@@ -12,8 +12,8 @@
  ** \brief Solving for handling exponential function.
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H
-#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H
+#ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H
+#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__SINE_SOLVER_H
 
 #include <map>
 
@@ -177,4 +177,4 @@ class SineSolver
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
+#endif /* CVC5__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h
index 8b7f5340d..4ecf5aa9a 100644
--- a/src/theory/arith/nl/transcendental/taylor_generator.h
+++ b/src/theory/arith/nl/transcendental/taylor_generator.h
@@ -12,8 +12,8 @@
  ** \brief Generate taylor approximations transcendental lemmas.
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H
-#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H
+#ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H
+#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H
 
 #include "expr/node.h"
 
@@ -120,4 +120,4 @@ class TaylorGenerator
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
+#endif /* CVC5__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h
index c3d098e03..1a2f59282 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.h
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.h
@@ -12,8 +12,8 @@
  ** \brief Solving for handling transcendental functions.
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H
-#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H
+#ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H
+#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H
 
 #include <vector>
 
@@ -202,4 +202,4 @@ class TranscendentalSolver
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
+#endif /* CVC5__THEORY__ARITH__TRANSCENDENTAL_SOLVER_H */
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h
index a55071ef1..3d1c4a037 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.h
+++ b/src/theory/arith/nl/transcendental/transcendental_state.h
@@ -12,8 +12,8 @@
  ** \brief Utilities for transcendental lemmas.
  **/
 
-#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H
-#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H
+#ifndef CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H
+#define CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H
 
 #include "expr/node.h"
 #include "expr/proof_set.h"
@@ -280,4 +280,4 @@ struct TranscendentalState
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H */
+#endif /* CVC5__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H */