Rename CVC4__ header guards to CVC5__. (#6326)

57 files changed, 149 insertions, 151 deletions

diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h
index 3e548f42d..d82fc9f0d 100644
--- a/src/theory/arith/arith_ite_utils.h
+++ b/src/theory/arith/arith_ite_utils.h
@@ -19,8 +19,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
-#define CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
+#ifndef CVC5__THEORY__ARITH__ARITH_ITE_UTILS_H
+#define CVC5__THEORY__ARITH__ARITH_ITE_UTILS_H
 
 #include <unordered_map>
 
@@ -113,4 +113,4 @@ private:
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H */
+#endif /* CVC5__THEORY__ARITH__ARITH_ITE_UTILS_H */
diff --git a/src/theory/arith/arith_msum.h b/src/theory/arith/arith_msum.h
index 7854e0d3b..c9ed61fe5 100644
--- a/src/theory/arith/arith_msum.h
+++ b/src/theory/arith/arith_msum.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__MSUM_H
-#define CVC4__THEORY__ARITH__MSUM_H
+#ifndef CVC5__THEORY__ARITH__MSUM_H
+#define CVC5__THEORY__ARITH__MSUM_H
 
 #include <map>
 
@@ -185,4 +185,4 @@ class ArithMSum
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__MSUM_H */
+#endif /* CVC5__THEORY__ARITH__MSUM_H */
diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h
index 663c09abe..82bf07b45 100644
--- a/src/theory/arith/arith_preprocess.h
+++ b/src/theory/arith/arith_preprocess.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__ARITH_PREPROCESS_H
-#define CVC4__THEORY__ARITH__ARITH_PREPROCESS_H
+#ifndef CVC5__THEORY__ARITH__ARITH_PREPROCESS_H
+#define CVC5__THEORY__ARITH__ARITH_PREPROCESS_H
 
 #include "context/cdhashmap.h"
 #include "theory/arith/operator_elim.h"
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 803f8c8a8..27b7cf9d2 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__ARITH_REWRITER_H
-#define CVC4__THEORY__ARITH__ARITH_REWRITER_H
+#ifndef CVC5__THEORY__ARITH__ARITH_REWRITER_H
+#define CVC5__THEORY__ARITH__ARITH_REWRITER_H
 
 #include "theory/arith/rewrites.h"
 #include "theory/theory_rewriter.h"
@@ -75,4 +75,4 @@ class ArithRewriter : public TheoryRewriter
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__ARITH_REWRITER_H */
+#endif /* CVC5__THEORY__ARITH__ARITH_REWRITER_H */
diff --git a/src/theory/arith/arith_state.h b/src/theory/arith/arith_state.h
index 05b09a5a2..1bf907f97 100644
--- a/src/theory/arith/arith_state.h
+++ b/src/theory/arith/arith_state.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__ARITH_STATE_H
-#define CVC4__THEORY__ARITH__ARITH_STATE_H
+#ifndef CVC5__THEORY__ARITH__ARITH_STATE_H
+#define CVC5__THEORY__ARITH__ARITH_STATE_H
 
 #include "theory/theory_state.h"
 
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index b96d7a86a..0e708f63e 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
-#define CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
+#ifndef CVC5__THEORY__ARITH__ARITH_STATIC_LEARNER_H
+#define CVC5__THEORY__ARITH__ARITH_STATIC_LEARNER_H
 
 #include "context/cdhashmap.h"
 #include "theory/arith/arith_utilities.h"
@@ -76,4 +76,4 @@ public:
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H */
+#endif /* CVC5__THEORY__ARITH__ARITH_STATIC_LEARNER_H */
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index c9f572364..337b18d9b 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__ARITH_UTILITIES_H
-#define CVC4__THEORY__ARITH__ARITH_UTILITIES_H
+#ifndef CVC5__THEORY__ARITH__ARITH_UTILITIES_H
+#define CVC5__THEORY__ARITH__ARITH_UTILITIES_H
 
 #include <unordered_map>
 #include <unordered_set>
@@ -334,4 +334,4 @@ Node negateProofLiteral(TNode n);
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__ARITH_UTILITIES_H */
+#endif /* CVC5__THEORY__ARITH__ARITH_UTILITIES_H */
diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h
index 6764e8e0b..f70c1d311 100644
--- a/src/theory/arith/arithvar_node_map.h
+++ b/src/theory/arith/arithvar_node_map.h
@@ -17,9 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
-#define CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
-
+#ifndef CVC5__THEORY__ARITH__ARITHVAR_NODE_MAP_H
+#define CVC5__THEORY__ARITH__ARITHVAR_NODE_MAP_H
 
 #include "theory/arith/arithvar.h"
 #include "context/context.h"
@@ -92,4 +91,4 @@ public:
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H */
+#endif /* CVC5__THEORY__ARITH__ARITHVAR_NODE_MAP_H */
diff --git a/src/theory/arith/bound_inference.h b/src/theory/arith/bound_inference.h
index fc5e68cff..b022dc7fc 100644
--- a/src/theory/arith/bound_inference.h
+++ b/src/theory/arith/bound_inference.h
@@ -12,8 +12,8 @@
  ** \brief Extract bounds on variables from theory atoms.
  **/
 
-#ifndef CVC4__THEORY__ARITH__BOUND_INFERENCE_H
-#define CVC4__THEORY__ARITH__BOUND_INFERENCE_H
+#ifndef CVC5__THEORY__ARITH__BOUND_INFERENCE_H
+#define CVC5__THEORY__ARITH__BOUND_INFERENCE_H
 
 #include <map>
 #include <utility>
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 33e39a5f0..67b64fc13 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -75,8 +75,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__CONSTRAINT_H
-#define CVC4__THEORY__ARITH__CONSTRAINT_H
+#ifndef CVC5__THEORY__ARITH__CONSTRAINT_H
+#define CVC5__THEORY__ARITH__CONSTRAINT_H
 
 #include <unordered_map>
 #include <vector>
@@ -1278,4 +1278,4 @@ private:
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__CONSTRAINT_H */
+#endif /* CVC5__THEORY__ARITH__CONSTRAINT_H */
diff --git a/src/theory/arith/constraint_forward.h b/src/theory/arith/constraint_forward.h
index 146ffd607..55c07b860 100644
--- a/src/theory/arith/constraint_forward.h
+++ b/src/theory/arith/constraint_forward.h
@@ -18,8 +18,8 @@
  ** between header files.
  **/
 
-#ifndef CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H
-#define CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H
+#ifndef CVC5__THEORY__ARITH__CONSTRAINT_FORWARD_H
+#define CVC5__THEORY__ARITH__CONSTRAINT_FORWARD_H
 
 #include "cvc4_private.h"
 #include <vector>
@@ -48,4 +48,4 @@ static const RationalVectorP RationalVectorPSentinel = NULL;
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H */
+#endif /* CVC5__THEORY__ARITH__CONSTRAINT_FORWARD_H */
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index 9b3106036..ed6c107cc 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -16,9 +16,8 @@
 
 #include "cvc4_private.h"
 
-
-#ifndef CVC4__THEORY__ARITH__DIO_SOLVER_H
-#define CVC4__THEORY__ARITH__DIO_SOLVER_H
+#ifndef CVC5__THEORY__ARITH__DIO_SOLVER_H
+#define CVC5__THEORY__ARITH__DIO_SOLVER_H
 
 #include <unordered_map>
 #include <utility>
@@ -425,4 +424,4 @@ public:
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__DIO_SOLVER_H */
+#endif /* CVC5__THEORY__ARITH__DIO_SOLVER_H */
diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h
index a5b200f8b..aaa601142 100644
--- a/src/theory/arith/inference_manager.h
+++ b/src/theory/arith/inference_manager.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
-#define CVC4__THEORY__ARITH__INFERENCE_MANAGER_H
+#ifndef CVC5__THEORY__ARITH__INFERENCE_MANAGER_H
+#define CVC5__THEORY__ARITH__INFERENCE_MANAGER_H
 
 #include <vector>
 
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 */
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 940812604..c4f702b43 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__NORMAL_FORM_H
-#define CVC4__THEORY__ARITH__NORMAL_FORM_H
+#ifndef CVC5__THEORY__ARITH__NORMAL_FORM_H
+#define CVC5__THEORY__ARITH__NORMAL_FORM_H
 
 #include <algorithm>
 
@@ -1406,4 +1406,4 @@ public:
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__NORMAL_FORM_H */
+#endif /* CVC5__THEORY__ARITH__NORMAL_FORM_H */
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 30a684e47..cef635395 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__PARTIAL_MODEL_H
-#define CVC4__THEORY__ARITH__PARTIAL_MODEL_H
+#ifndef CVC5__THEORY__ARITH__PARTIAL_MODEL_H
+#define CVC5__THEORY__ARITH__PARTIAL_MODEL_H
 
 #include <vector>
 
@@ -416,4 +416,4 @@ private:
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__PARTIAL_MODEL_H */
+#endif /* CVC5__THEORY__ARITH__PARTIAL_MODEL_H */
diff --git a/src/theory/arith/proof_checker.h b/src/theory/arith/proof_checker.h
index ca4fdfb6d..86251135c 100644
--- a/src/theory/arith/proof_checker.h
+++ b/src/theory/arith/proof_checker.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__PROOF_CHECKER_H
-#define CVC4__THEORY__ARITH__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__ARITH__PROOF_CHECKER_H
+#define CVC5__THEORY__ARITH__PROOF_CHECKER_H
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
@@ -45,4 +45,4 @@ class ArithProofRuleChecker : public ProofRuleChecker
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__ARITH__PROOF_CHECKER_H */
diff --git a/src/theory/arith/proof_macros.h b/src/theory/arith/proof_macros.h
index a02738fd3..32a31b157 100644
--- a/src/theory/arith/proof_macros.h
+++ b/src/theory/arith/proof_macros.h
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__PROOF_MACROS_H
-#define CVC4__THEORY__ARITH__PROOF_MACROS_H
+#ifndef CVC5__THEORY__ARITH__PROOF_MACROS_H
+#define CVC5__THEORY__ARITH__PROOF_MACROS_H
 
 #include "options/smt_options.h"
 
@@ -28,4 +28,4 @@
 #define ARITH_NULLPROOF(x) (cvc5::options::produceProofs()) ? x : NULL
 #define ARITH_PROOF_ON() cvc5::options::produceProofs()
 
-#endif  // CVC4__THEORY__ARITH__PROOF_MACROS_H
+#endif  // CVC5__THEORY__ARITH__PROOF_MACROS_H
diff --git a/src/theory/arith/rewrites.h b/src/theory/arith/rewrites.h
index e7a44f27e..2a85e6358 100644
--- a/src/theory/arith/rewrites.h
+++ b/src/theory/arith/rewrites.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__REWRITES_H
-#define CVC4__THEORY__ARITH__REWRITES_H
+#ifndef CVC5__THEORY__ARITH__REWRITES_H
+#define CVC5__THEORY__ARITH__REWRITES_H
 
 #include <iosfwd>
 
@@ -79,4 +79,4 @@ std::ostream& operator<<(std::ostream& out, Rewrite r);
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__REWRITES_H */
+#endif /* CVC5__THEORY__ARITH__REWRITES_H */
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index e8769064a..6d93c74dd 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
-#define CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
+#ifndef CVC5__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
+#define CVC5__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
 
 namespace cvc5 {
 namespace theory {
@@ -166,4 +166,4 @@ class IndexedRootPredicateTypeRule
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */
+#endif /* CVC5__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */
diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
index 9b3f4535b..d0ecdeda0 100644
--- a/src/theory/arith/type_enumerator.h
+++ b/src/theory/arith/type_enumerator.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
-#define CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
+#ifndef CVC5__THEORY__ARITH__TYPE_ENUMERATOR_H
+#define CVC5__THEORY__ARITH__TYPE_ENUMERATOR_H
 
 #include "expr/kind.h"
 #include "expr/type_node.h"
@@ -104,4 +104,4 @@ class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> {
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H */
+#endif /* CVC5__THEORY__ARITH__TYPE_ENUMERATOR_H */