Rename CVC4__ header guards to CVC5__. (#6326)

117 files changed, 312 insertions, 312 deletions

diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h
index 03047c93b..058d01672 100644
--- a/src/theory/quantifiers/alpha_equivalence.h
+++ b/src/theory/quantifiers/alpha_equivalence.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__ALPHA_EQUIVALENCE_H
-#define CVC4__ALPHA_EQUIVALENCE_H
+#ifndef CVC5__ALPHA_EQUIVALENCE_H
+#define CVC5__ALPHA_EQUIVALENCE_H
 
 #include "theory/quantifiers/quant_util.h"
 
diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h
index a187cd36a..1ae1b6fbc 100644
--- a/src/theory/quantifiers/bv_inverter.h
+++ b/src/theory/quantifiers/bv_inverter.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__BV_INVERTER_H
-#define CVC4__BV_INVERTER_H
+#ifndef CVC5__BV_INVERTER_H
+#define CVC5__BV_INVERTER_H
 
 #include <map>
 #include <unordered_map>
@@ -130,4 +130,4 @@ class BvInverter
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__BV_INVERTER_H */
+#endif /* CVC5__BV_INVERTER_H */
diff --git a/src/theory/quantifiers/bv_inverter_utils.h b/src/theory/quantifiers/bv_inverter_utils.h
index 823855d1b..2fbdf5b67 100644
--- a/src/theory/quantifiers/bv_inverter_utils.h
+++ b/src/theory/quantifiers/bv_inverter_utils.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__BV_INVERTER_UTILS_H
-#define CVC4__BV_INVERTER_UTILS_H
+#ifndef CVC5__BV_INVERTER_UTILS_H
+#define CVC5__BV_INVERTER_UTILS_H
 
 #include "expr/node.h"
 
diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h
index 45333bc76..459a0b6c0 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.h
+++ b/src/theory/quantifiers/candidate_rewrite_database.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
-#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
+#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
 
 #include <vector>
 
@@ -130,4 +130,4 @@ class CandidateRewriteDatabase : public ExprMiner
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */
diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h
index aa31c7845..d73160add 100644
--- a/src/theory/quantifiers/candidate_rewrite_filter.h
+++ b/src/theory/quantifiers/candidate_rewrite_filter.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
-#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
+#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H
 
 #include <map>
 #include "expr/match_trie.h"
@@ -173,4 +173,4 @@ class CandidateRewriteFilter
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
index a81f5f180..f6533c5cc 100644
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
-#define CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
+#define CVC5__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H
 
 #include <vector>
 #include "expr/node.h"
@@ -211,4 +211,4 @@ class ArithInstantiator : public Instantiator
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
index 9914428ef..5ce3c1fa4 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
-#define CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
+#define CVC5__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H
 
 #include <unordered_map>
 #include "theory/quantifiers/bv_inverter.h"
@@ -211,4 +211,4 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
index ac68dc4d5..364c6c0fc 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__BV_INSTANTIATOR_UTILS_H
-#define CVC4__BV_INSTANTIATOR_UTILS_H
+#ifndef CVC5__BV_INSTANTIATOR_UTILS_H
+#define CVC5__BV_INSTANTIATOR_UTILS_H
 
 #include "expr/attribute.h"
 #include "expr/node.h"
diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
index 27bf560cb..a7507a8ec 100644
--- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
-#define CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
+#define CVC5__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H
 
 #include "expr/node.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
@@ -93,4 +93,4 @@ class DtInstantiator : public Instantiator
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index 986874266..a1ca2f92c 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
-#define CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
+#define CVC5__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H
 
 #include <vector>
 
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index 85724a915..538eac2e1 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
-#define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
+#define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H
 
 #include "theory/decision_manager.h"
 #include "theory/quantifiers/bv_inverter.h"
diff --git a/src/theory/quantifiers/cegqi/nested_qe.h b/src/theory/quantifiers/cegqi/nested_qe.h
index e0cccb9c9..31d7fe1fe 100644
--- a/src/theory/quantifiers/cegqi/nested_qe.h
+++ b/src/theory/quantifiers/cegqi/nested_qe.h
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H
-#define CVC4__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H
+#define CVC5__THEORY__QUANTIFIERS__CEQGI__NESTED_QE_H
 
 #include <unordered_set>
 
diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.h b/src/theory/quantifiers/cegqi/vts_term_cache.h
index d56684d43..99b2952df 100644
--- a/src/theory/quantifiers/cegqi/vts_term_cache.h
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H
-#define CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H
+#define CVC5__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H
 
 #include <map>
 #include "expr/attribute.h"
@@ -142,4 +142,4 @@ class VtsTermCache
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H */
diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h
index 9fce59796..b45013a2c 100644
--- a/src/theory/quantifiers/dynamic_rewrite.h
+++ b/src/theory/quantifiers/dynamic_rewrite.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
-#define CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
+#define CVC5__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H
 
 #include <map>
 
@@ -121,4 +121,4 @@ class DynamicRewriter
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */
diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h
index 0de57f02f..ade813716 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.h
+++ b/src/theory/quantifiers/ematching/candidate_generator.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
-#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H
 
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -245,4 +245,4 @@ class CandidateGeneratorSelector : public CandidateGeneratorQE
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */
diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h
index 12c91be63..01271063a 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.h
+++ b/src/theory/quantifiers/ematching/ho_trigger.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H
-#define CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__HO_TRIGGER_H
+#define CVC5__THEORY__QUANTIFIERS__HO_TRIGGER_H
 
 #include <map>
 #include <unordered_set>
@@ -277,4 +277,4 @@ class HigherOrderTrigger : public Trigger
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__HO_TRIGGER_H */
diff --git a/src/theory/quantifiers/ematching/im_generator.h b/src/theory/quantifiers/ematching/im_generator.h
index 222e3c078..305990bf8 100644
--- a/src/theory/quantifiers/ematching/im_generator.h
+++ b/src/theory/quantifiers/ematching/im_generator.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__IM_GENERATOR_H
-#define CVC4__THEORY__QUANTIFIERS__IM_GENERATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__IM_GENERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__IM_GENERATOR_H
 
 #include <map>
 #include "expr/node.h"
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h
index 7b440035f..ae389e0ce 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
-#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H
 
 #include <map>
 #include "expr/node.h"
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.h b/src/theory/quantifiers/ematching/inst_match_generator_multi.h
index 309aa2640..7d870e566 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H
-#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H
+#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_H
 
 #include <map>
 #include <vector>
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 4d4339bac..ac15b1752 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H
-#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H
+#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_MULTI_LINEAR_H
 
 #include <vector>
 
diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.h b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
index ccc650044..6c2bec0f0 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator_simple.h
+++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H
-#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H
+#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_SIMPLE_H
 
 #include <map>
 #include <vector>
diff --git a/src/theory/quantifiers/ematching/inst_strategy.h b/src/theory/quantifiers/ematching/inst_strategy.h
index 1ce62f170..405bf0a4d 100644
--- a/src/theory/quantifiers/ematching/inst_strategy.h
+++ b/src/theory/quantifiers/ematching/inst_strategy.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_H
-#define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_H
+#define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_H
 
 #include <vector>
 #include "expr/node.h"
@@ -87,4 +87,4 @@ class InstStrategy
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
index 2c765e194..62b4b2623 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__INST_STRATEGY_E_MATCHING_H
-#define CVC4__INST_STRATEGY_E_MATCHING_H
+#ifndef CVC5__INST_STRATEGY_E_MATCHING_H
+#define CVC5__INST_STRATEGY_E_MATCHING_H
 
 #include "theory/quantifiers/ematching/inst_strategy.h"
 #include "theory/quantifiers/ematching/trigger.h"
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
index ed247b89a..cd037415c 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__INST_STRATEGY_E_MATCHING_USER_H
-#define CVC4__INST_STRATEGY_E_MATCHING_USER_H
+#ifndef CVC5__INST_STRATEGY_E_MATCHING_USER_H
+#define CVC5__INST_STRATEGY_E_MATCHING_USER_H
 
 #include <map>
 #include "expr/node.h"
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h
index bd7388afb..fc5a33164 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.h
+++ b/src/theory/quantifiers/ematching/instantiation_engine.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
-#define CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
+#define CVC5__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H
 
 #include <vector>
 
@@ -77,4 +77,4 @@ class InstantiationEngine : public QuantifiersModule {
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */
diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.h b/src/theory/quantifiers/ematching/pattern_term_selector.h
index 5ac6c1da3..e5209eeb1 100644
--- a/src/theory/quantifiers/ematching/pattern_term_selector.h
+++ b/src/theory/quantifiers/ematching/pattern_term_selector.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H
-#define CVC4__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H
+#define CVC5__THEORY__QUANTIFIERS__PATTERN_TERM_SELECTOR_H
 
 #include <map>
 
diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h
index e2ad00561..9ce4be544 100644
--- a/src/theory/quantifiers/ematching/trigger.h
+++ b/src/theory/quantifiers/ematching/trigger.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_H
-#define CVC4__THEORY__QUANTIFIERS__TRIGGER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_H
+#define CVC5__THEORY__QUANTIFIERS__TRIGGER_H
 
 #include "expr/node.h"
 #include "theory/inference_id.h"
@@ -221,4 +221,4 @@ class Trigger {
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TRIGGER_H */
diff --git a/src/theory/quantifiers/ematching/trigger_database.h b/src/theory/quantifiers/ematching/trigger_database.h
index 9cebb6173..8db50ae50 100644
--- a/src/theory/quantifiers/ematching/trigger_database.h
+++ b/src/theory/quantifiers/ematching/trigger_database.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H
-#define CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H
+#define CVC5__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H
 
 #include <vector>
 
@@ -107,4 +107,4 @@ class TriggerDatabase
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TRIGGER_DATABASE_H */
diff --git a/src/theory/quantifiers/ematching/trigger_term_info.h b/src/theory/quantifiers/ematching/trigger_term_info.h
index c70257e08..ad1dd967a 100644
--- a/src/theory/quantifiers/ematching/trigger_term_info.h
+++ b/src/theory/quantifiers/ematching/trigger_term_info.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H
-#define CVC4__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H
+#define CVC5__THEORY__QUANTIFIERS__TRIGGER_TERM_INFO_H
 
 #include <map>
 
diff --git a/src/theory/quantifiers/ematching/trigger_trie.h b/src/theory/quantifiers/ematching/trigger_trie.h
index fe16e3c0f..2fd39e9ef 100644
--- a/src/theory/quantifiers/ematching/trigger_trie.h
+++ b/src/theory/quantifiers/ematching/trigger_trie.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H
-#define CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TRIGGER_TRIE_H
+#define CVC5__THEORY__QUANTIFIERS__TRIGGER_TRIE_H
 
 #include <vector>
 
@@ -60,4 +60,4 @@ class TriggerTrie
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_TRIE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TRIGGER_TRIE_H */
diff --git a/src/theory/quantifiers/ematching/var_match_generator.h b/src/theory/quantifiers/ematching/var_match_generator.h
index 87c4d1e32..66f166cd1 100644
--- a/src/theory/quantifiers/ematching/var_match_generator.h
+++ b/src/theory/quantifiers/ematching/var_match_generator.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
-#define CVC4__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__VAR_MATCH_GENERATOR_H
 
 #include "expr/node.h"
 #include "theory/quantifiers/ematching/inst_match_generator.h"
diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h
index 988291ed5..f908c2a97 100644
--- a/src/theory/quantifiers/equality_query.h
+++ b/src/theory/quantifiers/equality_query.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
-#define CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
+#ifndef CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
+#define CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H
 
 #include "context/cdo.h"
 #include "context/context.h"
@@ -92,4 +92,4 @@ class EqualityQuery : public QuantifiersUtil
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */
+#endif /* CVC5__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */
diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index 37d0de6f8..aa1c9a1bf 100644
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
-#define CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
+#define CVC5__THEORY__QUANTIFIERS__EXPRESSION_MINER_H
 
 #include <map>
 #include <memory>
@@ -92,4 +92,4 @@ class ExprMiner
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__EXPRESSION_MINER_H */
diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h
index d33c9902c..b762f7625 100644
--- a/src/theory/quantifiers/expr_miner_manager.h
+++ b/src/theory/quantifiers/expr_miner_manager.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H
-#define CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H
+#define CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H
 
 #include "expr/node.h"
 #include "theory/quantifiers/candidate_rewrite_database.h"
@@ -120,4 +120,4 @@ class ExpressionMinerManager
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H */
diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h
index 0d6ece71e..a9d9e8b50 100644
--- a/src/theory/quantifiers/extended_rewrite.h
+++ b/src/theory/quantifiers/extended_rewrite.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
-#define CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
+#define CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
 
 #include <unordered_map>
 
@@ -252,4 +252,4 @@ class ExtendedRewriter
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index ec3b6dd7a..627b960a3 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__FIRST_ORDER_MODEL_H
-#define CVC4__FIRST_ORDER_MODEL_H
+#ifndef CVC5__FIRST_ORDER_MODEL_H
+#define CVC5__FIRST_ORDER_MODEL_H
 
 #include "context/cdlist.h"
 #include "theory/quantifiers/equality_query.h"
@@ -198,4 +198,4 @@ class FirstOrderModel : public TheoryModel
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__FIRST_ORDER_MODEL_H */
+#endif /* CVC5__FIRST_ORDER_MODEL_H */
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h
index fc6fac92a..e4b5a6083 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.h
+++ b/src/theory/quantifiers/fmf/bounded_integers.h
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__BOUNDED_INTEGERS_H
-#define CVC4__BOUNDED_INTEGERS_H
+#ifndef CVC5__BOUNDED_INTEGERS_H
+#define CVC5__BOUNDED_INTEGERS_H
 
 #include "theory/quantifiers/quant_module.h"
 
diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.h b/src/theory/quantifiers/fmf/first_order_model_fmc.h
index d858e24f6..b32e4dffa 100644
--- a/src/theory/quantifiers/fmf/first_order_model_fmc.h
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H
-#define CVC4__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H
+#ifndef CVC5__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H
+#define CVC5__THEORY__QUANTIFIERS__FMF__FIRST_ORDER_MODEL_FMC_H
 
 #include "theory/quantifiers/first_order_model.h"
 
@@ -56,4 +56,4 @@ class FirstOrderModelFmc : public FirstOrderModel
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__FIRST_ORDER_MODEL_H */
+#endif /* CVC5__FIRST_ORDER_MODEL_H */
diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index 586bde226..73ce86add 100644
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
-#define CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
+#ifndef CVC5__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
+#define CVC5__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H
 
 #include "theory/quantifiers/fmf/first_order_model_fmc.h"
 #include "theory/quantifiers/fmf/model_builder.h"
@@ -189,4 +189,4 @@ protected:
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index 4a95a8a73..94eab1fd6 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
-#define CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__MODEL_BUILDER_H
+#define CVC5__THEORY__QUANTIFIERS__MODEL_BUILDER_H
 
 #include "expr/node.h"
 #include "theory/quantifiers/inst_match.h"
@@ -75,4 +75,4 @@ class QModelBuilder : public TheoryEngineModelBuilder
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__MODEL_BUILDER_H */
diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h
index 5a983d726..112d21925 100644
--- a/src/theory/quantifiers/fmf/model_engine.h
+++ b/src/theory/quantifiers/fmf/model_engine.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H
-#define CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H
+#define CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H
 
 #include "theory/quantifiers/fmf/model_builder.h"
 #include "theory/quantifiers/quant_module.h"
@@ -73,4 +73,4 @@ private:
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__MODEL_ENGINE_H */
diff --git a/src/theory/quantifiers/fun_def_evaluator.h b/src/theory/quantifiers/fun_def_evaluator.h
index fcc30948d..a7aa22efd 100644
--- a/src/theory/quantifiers/fun_def_evaluator.h
+++ b/src/theory/quantifiers/fun_def_evaluator.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__QUANTIFIERS_FUN_DEF_EVALUATOR_H
-#define CVC4__QUANTIFIERS_FUN_DEF_EVALUATOR_H
+#ifndef CVC5__QUANTIFIERS_FUN_DEF_EVALUATOR_H
+#define CVC5__QUANTIFIERS_FUN_DEF_EVALUATOR_H
 
 #include <map>
 #include <vector>
diff --git a/src/theory/quantifiers/index_trie.h b/src/theory/quantifiers/index_trie.h
index 2c968e107..a10a31fe8 100644
--- a/src/theory/quantifiers/index_trie.h
+++ b/src/theory/quantifiers/index_trie.h
@@ -13,8 +13,8 @@
  ** that are not yielding  useful instantiations. of quantifier instantiation.
  ** This is used in the term_tuple_enumerator.
  **/
-#ifndef CVC4__THEORY__QUANTIFIERS__INDEX_TRIE_H
-#define CVC4__THEORY__QUANTIFIERS__INDEX_TRIE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INDEX_TRIE_H
+#define CVC5__THEORY__QUANTIFIERS__INDEX_TRIE_H
 #include <algorithm>
 #include <utility>
 #include <vector>
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index e5e8f97cd..7002e2858 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
-#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_H
+#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_H
 
 #include <vector>
 
@@ -91,4 +91,4 @@ inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__INST_MATCH_H */
diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h
index ca878c888..2f1dbb6d9 100644
--- a/src/theory/quantifiers/inst_match_trie.h
+++ b/src/theory/quantifiers/inst_match_trie.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
-#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
+#define CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H
 
 #include <map>
 
@@ -226,4 +226,4 @@ class InstMatchTrieOrdered
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H */
diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h
index 7b5cb8e0e..39f719ced 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.h
+++ b/src/theory/quantifiers/inst_strategy_enumerative.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__INST_STRATEGY_ENUMERATIVE_H
-#define CVC4__INST_STRATEGY_ENUMERATIVE_H
+#ifndef CVC5__INST_STRATEGY_ENUMERATIVE_H
+#define CVC5__INST_STRATEGY_ENUMERATIVE_H
 
 #include "theory/quantifiers/quant_module.h"
 
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index b56938fd1..7ec4d837a 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
-#define CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H
+#define CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H
 
 #include <map>
 
@@ -363,4 +363,4 @@ class Instantiate : public QuantifiersUtil
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__INSTANTIATE_H */
diff --git a/src/theory/quantifiers/instantiation_list.h b/src/theory/quantifiers/instantiation_list.h
index 86dfa0081..e6915418b 100644
--- a/src/theory/quantifiers/instantiation_list.h
+++ b/src/theory/quantifiers/instantiation_list.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H
-#define CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H
+#define CVC5__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H
 
 #include <iosfwd>
 #include <vector>
@@ -55,4 +55,4 @@ std::ostream& operator<<(std::ostream& out, const SkolemList& skl);
 
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__INSTANTIATION_LIST_H */
diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h
index d4437ae75..f319ccf3b 100644
--- a/src/theory/quantifiers/lazy_trie.h
+++ b/src/theory/quantifiers/lazy_trie.h
@@ -12,8 +12,8 @@
  ** \brief lazy trie
  **/
 
-#ifndef CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H
-#define CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__LAZY_TRIE_H
+#define CVC5__THEORY__QUANTIFIERS__LAZY_TRIE_H
 
 #include "expr/node.h"
 
@@ -170,4 +170,4 @@ class LazyTrieMulti
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__LAZY_TRIE_H */
diff --git a/src/theory/quantifiers/proof_checker.h b/src/theory/quantifiers/proof_checker.h
index 39e933149..66a4b30ae 100644
--- a/src/theory/quantifiers/proof_checker.h
+++ b/src/theory/quantifiers/proof_checker.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__PROOF_CHECKER_H
-#define CVC4__THEORY__QUANTIFIERS__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__PROOF_CHECKER_H
+#define CVC5__THEORY__QUANTIFIERS__PROOF_CHECKER_H
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
@@ -46,4 +46,4 @@ class QuantifiersProofRuleChecker : public ProofRuleChecker
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__PROOF_CHECKER_H */
diff --git a/src/theory/quantifiers/quant_bound_inference.h b/src/theory/quantifiers/quant_bound_inference.h
index 7c15d5146..6533bb8e9 100644
--- a/src/theory/quantifiers/quant_bound_inference.h
+++ b/src/theory/quantifiers/quant_bound_inference.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H
-#define CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H
+#define CVC5__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H
 
 #include <vector>
 #include "expr/node.h"
@@ -124,4 +124,4 @@ class QuantifiersBoundInference
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__QUANT_BOUND_INFERENCE_H */
diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h
index 01a51ccff..1f238a016 100644
--- a/src/theory/quantifiers/quant_module.h
+++ b/src/theory/quantifiers/quant_module.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANT_MODULE_H
-#define CVC4__THEORY__QUANT_MODULE_H
+#ifndef CVC5__THEORY__QUANT_MODULE_H
+#define CVC5__THEORY__QUANT_MODULE_H
 
 #include <iostream>
 #include <map>
@@ -179,4 +179,4 @@ class QuantifiersModule
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANT_UTIL_H */
+#endif /* CVC5__THEORY__QUANT_UTIL_H */
diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h
index e6a178c73..4638a061e 100644
--- a/src/theory/quantifiers/quant_relevance.h
+++ b/src/theory/quantifiers/quant_relevance.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANT_RELEVANCE_H
-#define CVC4__THEORY__QUANT_RELEVANCE_H
+#ifndef CVC5__THEORY__QUANT_RELEVANCE_H
+#define CVC5__THEORY__QUANT_RELEVANCE_H
 
 #include <map>
 
@@ -65,4 +65,4 @@ class QuantRelevance : public QuantifiersUtil
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANT_RELEVANCE_H */
+#endif /* CVC5__THEORY__QUANT_RELEVANCE_H */
diff --git a/src/theory/quantifiers/quant_rep_bound_ext.h b/src/theory/quantifiers/quant_rep_bound_ext.h
index 6fe0faefa..df0cd2fd7 100644
--- a/src/theory/quantifiers/quant_rep_bound_ext.h
+++ b/src/theory/quantifiers/quant_rep_bound_ext.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H
-#define CVC4__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H
+#define CVC5__THEORY__QUANTIFIERS__QUANT_REP_BOUND_EXT_H
 
 #include <map>
 
@@ -69,4 +69,4 @@ class QRepBoundExt : public RepBoundExt
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__FIRST_ORDER_MODEL_H */
+#endif /* CVC5__FIRST_ORDER_MODEL_H */
diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index ee961cbbc..de3086cca 100644
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANT_SPLIT_H
-#define CVC4__THEORY__QUANT_SPLIT_H
+#ifndef CVC5__THEORY__QUANT_SPLIT_H
+#define CVC5__THEORY__QUANT_SPLIT_H
 
 #include "context/cdo.h"
 #include "theory/quantifiers/quant_module.h"
diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 90955226c..3fb152a51 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANT_UTIL_H
-#define CVC4__THEORY__QUANT_UTIL_H
+#ifndef CVC5__THEORY__QUANT_UTIL_H
+#define CVC5__THEORY__QUANT_UTIL_H
 
 #include <iostream>
 #include <map>
@@ -82,4 +82,4 @@ public:
 }
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANT_UTIL_H */
+#endif /* CVC5__THEORY__QUANT_UTIL_H */
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 2fb294abe..9bbe0e271 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
-#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
+#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H
 
 #include "expr/attribute.h"
 #include "expr/node.h"
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h
index b468e0478..3072cc90d 100644
--- a/src/theory/quantifiers/quantifiers_inference_manager.h
+++ b/src/theory/quantifiers/quantifiers_inference_manager.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H
-#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H
+#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H
 
 #include "theory/inference_manager_buffered.h"
 #include "theory/quantifiers/quantifiers_state.h"
@@ -61,4 +61,4 @@ class QuantifiersInferenceManager : public InferenceManagerBuffered
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_INFERENCE_MANAGER_H */
diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h
index c52da79a7..745ff7bbd 100644
--- a/src/theory/quantifiers/quantifiers_modules.h
+++ b/src/theory/quantifiers/quantifiers_modules.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H
-#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H
+#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H
 
 #include "theory/quantifiers/alpha_equivalence.h"
 #include "theory/quantifiers/conjecture_generator.h"
@@ -96,4 +96,4 @@ class QuantifiersModules
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MODULES_H */
diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h
index 383934c15..b8479596d 100644
--- a/src/theory/quantifiers/quantifiers_registry.h
+++ b/src/theory/quantifiers/quantifiers_registry.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
-#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
+#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
 
 #include "expr/node.h"
 #include "theory/quantifiers/quant_bound_inference.h"
@@ -131,4 +131,4 @@ class QuantifiersRegistry : public QuantifiersUtil
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index c45bc9e88..4b55d3e17 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
-#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
+#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
 
 #include "theory/theory_rewriter.h"
 #include "theory/trust_node.h"
@@ -305,4 +305,4 @@ public:
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */
diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h
index 623d52289..d540923ac 100644
--- a/src/theory/quantifiers/quantifiers_state.h
+++ b/src/theory/quantifiers/quantifiers_state.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
-#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
+#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H
 
 #include "theory/quantifiers/quantifiers_statistics.h"
 #include "theory/theory.h"
@@ -88,4 +88,4 @@ class QuantifiersState : public TheoryState
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H */
diff --git a/src/theory/quantifiers/quantifiers_statistics.h b/src/theory/quantifiers/quantifiers_statistics.h
index 9eccf3ce6..8ff97d83e 100644
--- a/src/theory/quantifiers/quantifiers_statistics.h
+++ b/src/theory/quantifiers/quantifiers_statistics.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
-#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
+#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
 
 #include "util/statistics_registry.h"
 #include "util/stats_timer.h"
@@ -49,4 +49,4 @@ class QuantifiersStatistics
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H */
diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h
index cf10b42da..b3f1fae54 100644
--- a/src/theory/quantifiers/query_generator.h
+++ b/src/theory/quantifiers/query_generator.h
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
-#define CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__QUERY_GENERATOR_H
 
 #include <map>
 #include <unordered_set>
@@ -118,4 +118,4 @@ class QueryGenerator : public ExprMiner
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS___H */
+#endif /* CVC5__THEORY__QUANTIFIERS___H */
diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index 807e4c4a2..f9958763c 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
-#define CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
+#ifndef CVC5__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
+#define CVC5__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
 
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quant_util.h"
@@ -172,4 +172,4 @@ class RelevantDomain : public QuantifiersUtil
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */
diff --git a/src/theory/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h
index 604c711ad..caf24acfe 100644
--- a/src/theory/quantifiers/single_inv_partition.h
+++ b/src/theory/quantifiers/single_inv_partition.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
-#define CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
+#define CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
 
 #include <map>
 #include <vector>
@@ -294,4 +294,4 @@ class SingleInvocationPartition
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */
diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index 4c4d770f3..f92627138 100644
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H
-#define CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H
+#define CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H
 
 #include <unordered_map>
 #include <unordered_set>
@@ -159,4 +159,4 @@ class Skolemize
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H */
diff --git a/src/theory/quantifiers/solution_filter.h b/src/theory/quantifiers/solution_filter.h
index bf3d9bddc..5b191b2be 100644
--- a/src/theory/quantifiers/solution_filter.h
+++ b/src/theory/quantifiers/solution_filter.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H
-#define CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SOLUTION_FILTER_H
+#define CVC5__THEORY__QUANTIFIERS__SOLUTION_FILTER_H
 
 #include <map>
 #include <unordered_set>
@@ -72,4 +72,4 @@ class SolutionFilterStrength : public ExprMiner
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SOLUTION_FILTER_H */
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
index ca83bf973..d9a3a3b02 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
-#define CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
+#define CVC5__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H
 
 #include "context/cdlist.h"
 #include "expr/subs.h"
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index f728d3d7e..883151fe6 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__CEGIS_H
-#define CVC4__THEORY__QUANTIFIERS__CEGIS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CEGIS_H
+#define CVC5__THEORY__QUANTIFIERS__CEGIS_H
 
 #include <map>
 #include "theory/quantifiers/sygus/sygus_module.h"
@@ -229,4 +229,4 @@ class Cegis : public SygusModule
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__CEGIS_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CEGIS_H */
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h
index 2abce835a..0f42ee13a 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.h
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H
-#define CVC4__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H
+#define CVC5__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H
 
 #include <unordered_set>
 
@@ -401,4 +401,4 @@ class CegisCoreConnective : public Cegis
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index a543bfda0..16a255cc9 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -13,8 +13,8 @@
  **/
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H
 
 #include <map>
 #include <vector>
diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h
index a72481a38..15aeb1cef 100644
--- a/src/theory/quantifiers/sygus/enum_stream_substitution.h
+++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h
@@ -14,8 +14,8 @@
  **/
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
 
 #include "expr/node.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
diff --git a/src/theory/quantifiers/sygus/example_eval_cache.h b/src/theory/quantifiers/sygus/example_eval_cache.h
index 1a70369a5..4f9fb0810 100644
--- a/src/theory/quantifiers/sygus/example_eval_cache.h
+++ b/src/theory/quantifiers/sygus/example_eval_cache.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H
-#define CVC4__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H
+#define CVC5__THEORY__QUANTIFIERS__EXAMPLE_EVAL_CACHE_H
 
 #include "expr/node_trie.h"
 #include "theory/quantifiers/sygus/example_infer.h"
diff --git a/src/theory/quantifiers/sygus/example_infer.h b/src/theory/quantifiers/sygus/example_infer.h
index dd2bf8a0a..06425df5a 100644
--- a/src/theory/quantifiers/sygus/example_infer.h
+++ b/src/theory/quantifiers/sygus/example_infer.h
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__EXAMPLE_INFER_H
-#define CVC4__THEORY__QUANTIFIERS__EXAMPLE_INFER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_INFER_H
+#define CVC5__THEORY__QUANTIFIERS__EXAMPLE_INFER_H
 
 #include "theory/quantifiers/sygus/sygus_unif_io.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
diff --git a/src/theory/quantifiers/sygus/example_min_eval.h b/src/theory/quantifiers/sygus/example_min_eval.h
index 2105faf2b..00db03b73 100644
--- a/src/theory/quantifiers/sygus/example_min_eval.h
+++ b/src/theory/quantifiers/sygus/example_min_eval.h
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H
-#define CVC4__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H
+#ifndef CVC5__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H
+#define CVC5__THEORY__QUANTIFIERS__EXAMPLE_MIN_EVAL_H
 
 #include <vector>
 
diff --git a/src/theory/quantifiers/sygus/rcons_obligation_info.h b/src/theory/quantifiers/sygus/rcons_obligation_info.h
index 3bded2a90..1de76cae8 100644
--- a/src/theory/quantifiers/sygus/rcons_obligation_info.h
+++ b/src/theory/quantifiers/sygus/rcons_obligation_info.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
-#define CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
+#ifndef CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
+#define CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
 
 #include "expr/node.h"
 
@@ -147,4 +147,4 @@ class RConsObligationInfo
 }  // namespace theory
 }  // namespace cvc5
 
-#endif  // CVC4__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
+#endif  // CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_INFO_H
diff --git a/src/theory/quantifiers/sygus/rcons_type_info.h b/src/theory/quantifiers/sygus/rcons_type_info.h
index 974897023..353165405 100644
--- a/src/theory/quantifiers/sygus/rcons_type_info.h
+++ b/src/theory/quantifiers/sygus/rcons_type_info.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
-#define CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
+#ifndef CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
+#define CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
 
 #include "theory/quantifiers/sygus/sygus_enumerator.h"
 
@@ -99,4 +99,4 @@ class RConsTypeInfo
 }  // namespace theory
 }  // namespace cvc5
 
-#endif  // CVC4__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
+#endif  // CVC5__THEORY__QUANTIFIERS__RCONS_TYPE_INFO_H
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.h b/src/theory/quantifiers/sygus/sygus_abduct.h
index 634a9a4bd..c1239acfa 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.h
+++ b/src/theory/quantifiers/sygus/sygus_abduct.h
@@ -13,8 +13,8 @@
  ** abduction problem.
  **/
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H
 
 #include <string>
 #include <vector>
@@ -87,4 +87,4 @@ class SygusAbduct
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_ABDUCT_H */
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h
index f1ef115f8..788378467 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H
 
 #include <map>
 #include <unordered_set>
@@ -508,4 +508,4 @@ class SygusEnumerator : public EnumValGenerator
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h
index 1f489eafc..d4d5e8354 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator_basic.h
+++ b/src/theory/quantifiers/sygus/sygus_enumerator_basic.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H
 
 #include <map>
 #include <unordered_set>
@@ -67,4 +67,4 @@ class EnumValGeneratorBasic : public EnumValGenerator
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_BASIC_H */
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h
index 628f01c40..edbd53d48 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H
 
 #include <map>
 #include "expr/node.h"
@@ -156,4 +156,4 @@ class SygusEvalUnfold
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */
diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h
index 477857794..3da36f603 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.h
+++ b/src/theory/quantifiers/sygus/sygus_explain.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
 
 #include <vector>
 
@@ -243,4 +243,4 @@ class SygusExplain
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index 56f469fef..d028a2a76 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H
 
 #include <map>
 #include <vector>
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index eda34a251..eba97bbc6 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
@@ -14,8 +14,8 @@
  **/
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H
 
 #include <map>
 #include <memory>
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h
index 2144102e0..e90455274 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H
 
 #include <map>
 #include <vector>
@@ -120,4 +120,4 @@ class SygusRedundantCons
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h
index c63d096b8..46ebc316d 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.h
+++ b/src/theory/quantifiers/sygus/sygus_interpol.h
@@ -13,8 +13,8 @@
  ** conjecture into an interpolation problem, and solve it.
  **/
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H
 
 #include <string>
 #include <vector>
@@ -215,4 +215,4 @@ class SygusInterpol
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H */
diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h
index df2e189e3..4395c01c1 100644
--- a/src/theory/quantifiers/sygus/sygus_invariance.h
+++ b/src/theory/quantifiers/sygus/sygus_invariance.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
 
 #include <unordered_map>
 #include <vector>
@@ -300,4 +300,4 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index 90460eeed..87ce27ac4 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H
 
 #include <vector>
 
@@ -159,4 +159,4 @@ class SygusModule
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_MODULE_H */
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index a56a22838..263db20fc 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_PBE_H
 
 #include "theory/quantifiers/sygus/sygus_module.h"
 
diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h
index 6f6e25d0c..ca00a0ec3 100644
--- a/src/theory/quantifiers/sygus/sygus_process_conj.h
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.h
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H
 
 #include <map>
 #include <unordered_map>
diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
index 26bbf2f92..c1d9bf85c 100644
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
@@ -12,8 +12,8 @@
  ** \brief Sygus quantifier elimination preprocessor
  **/
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H
 
 #include "expr/node.h"
 
@@ -47,4 +47,4 @@ class SygusQePreproc
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_QE_PREPROC_H */
diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h
index 1f9037a26..433f20d23 100644
--- a/src/theory/quantifiers/sygus/sygus_reconstruct.h
+++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
 
 #include <map>
 #include <vector>
@@ -309,4 +309,4 @@ class SygusReconstruct : public expr::NotifyMatch
 }  // namespace theory
 }  // namespace cvc5
 
-#endif  // CVC4__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
+#endif  // CVC5__THEORY__QUANTIFIERS__SYGUS_RECONSTRUCT_H
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h
index b79fa4177..1df5ab821 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.h
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
 
 #include <unordered_set>
 #include "expr/node.h"
@@ -211,4 +211,4 @@ class SygusRepairConst
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */
diff --git a/src/theory/quantifiers/sygus/sygus_stats.h b/src/theory/quantifiers/sygus/sygus_stats.h
index 7a8ae8ce9..d8a487d2f 100644
--- a/src/theory/quantifiers/sygus/sygus_stats.h
+++ b/src/theory/quantifiers/sygus/sygus_stats.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_STATS_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_STATS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H
 
 #include "util/statistics_registry.h"
 
diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
index 1ed81194a..ccd803731 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.h
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H
 
 #include <map>
 #include "expr/node.h"
@@ -195,4 +195,4 @@ class SygusUnif
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h
index 825e5741d..5fdcdcf35 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_io.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_io.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H
 
 #include <map>
 #include "theory/quantifiers/sygus/sygus_unif.h"
@@ -470,4 +470,4 @@ class SygusUnifIo : public SygusUnif
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index 51c49cbef..e61ac5b73 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H
 
 #include <map>
 #include "options/main_options.h"
@@ -445,4 +445,4 @@ class SygusUnifRl : public SygusUnif
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h
index 2508fdc9b..39b2fc80c 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
 
 #include <map>
 #include "expr/node.h"
@@ -430,4 +430,4 @@ class SygusUnifStrategy
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_H */
diff --git a/src/theory/quantifiers/sygus/sygus_utils.h b/src/theory/quantifiers/sygus/sygus_utils.h
index 0ec497789..28ef682e1 100644
--- a/src/theory/quantifiers/sygus/sygus_utils.h
+++ b/src/theory/quantifiers/sygus/sygus_utils.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H
 
 #include <vector>
 
@@ -112,4 +112,4 @@ class SygusUtils
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H */
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 7fd1ae4b3..2d462426b 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
-#define CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
+#define CVC5__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H
 
 #include <memory>
 
diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h
index a5fde8476..a590e930c 100644
--- a/src/theory/quantifiers/sygus/synth_engine.h
+++ b/src/theory/quantifiers/sygus/synth_engine.h
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
-#define CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
+#define CVC5__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
 
 #include "context/cdhashmap.h"
 #include "theory/quantifiers/quant_module.h"
diff --git a/src/theory/quantifiers/sygus/template_infer.h b/src/theory/quantifiers/sygus/template_infer.h
index 1ab97b651..f8c8e3c17 100644
--- a/src/theory/quantifiers/sygus/template_infer.h
+++ b/src/theory/quantifiers/sygus/template_infer.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__TEMPLATE_INFER_H
 
 #include <map>
 
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index fb7e38ff8..fc937c73e 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
-#define CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
+#define CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H
 
 #include <unordered_set>
 
@@ -469,4 +469,4 @@ class TermDbSygus {
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H */
diff --git a/src/theory/quantifiers/sygus/transition_inference.h b/src/theory/quantifiers/sygus/transition_inference.h
index 8ddc1a320..b38752cb9 100644
--- a/src/theory/quantifiers/sygus/transition_inference.h
+++ b/src/theory/quantifiers/sygus/transition_inference.h
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H
-#define CVC4__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H
+#define CVC5__THEORY__QUANTIFIERS__TRANSITION_INFERENCE_H
 
 #include <map>
 #include <vector>
diff --git a/src/theory/quantifiers/sygus/type_info.h b/src/theory/quantifiers/sygus/type_info.h
index 79413a03c..444b61927 100644
--- a/src/theory/quantifiers/sygus/type_info.h
+++ b/src/theory/quantifiers/sygus/type_info.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H
 
 #include <map>
 
@@ -255,4 +255,4 @@ class SygusTypeInfo
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_INFO_H */
diff --git a/src/theory/quantifiers/sygus/type_node_id_trie.h b/src/theory/quantifiers/sygus/type_node_id_trie.h
index 6311cbabe..7b3ca4a70 100644
--- a/src/theory/quantifiers/sygus/type_node_id_trie.h
+++ b/src/theory/quantifiers/sygus/type_node_id_trie.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H
 
 #include <map>
 #include <vector>
@@ -50,4 +50,4 @@ class TypeNodeIdTrie
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS__TYPE_NODE_ID_TRIE_H */
diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h
index 35b66437b..70dae5a74 100644
--- a/src/theory/quantifiers/sygus_inst.h
+++ b/src/theory/quantifiers/sygus_inst.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_INST_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_INST_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INST_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_INST_H
 
 #include <unordered_map>
 #include <unordered_set>
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index 7350f4845..932eae041 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
-#define CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
+#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
+#define CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
 
 #include <map>
 #include "theory/evaluator.h"
@@ -322,4 +322,4 @@ class SygusSampler : public LazyTrieEvaluator
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 2077b3d2d..818e10c71 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
-#define CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H
+#define CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H
 
 #include <map>
 #include <unordered_map>
@@ -424,4 +424,4 @@ class TermDb : public QuantifiersUtil {
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H */
diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h
index bd545ff50..2257d3b60 100644
--- a/src/theory/quantifiers/term_enumeration.h
+++ b/src/theory/quantifiers/term_enumeration.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
-#define CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
+#define CVC5__THEORY__QUANTIFIERS__TERM_ENUMERATION_H
 
 #include <unordered_map>
 #include <vector>
@@ -73,4 +73,4 @@ class TermEnumeration
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */
diff --git a/src/theory/quantifiers/term_pools.h b/src/theory/quantifiers/term_pools.h
index 117cffc42..f97b84756 100644
--- a/src/theory/quantifiers/term_pools.h
+++ b/src/theory/quantifiers/term_pools.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H
-#define CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H
+#define CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H
 
 #include <unordered_set>
 #include <vector>
@@ -104,4 +104,4 @@ class TermPools : public QuantifiersUtil
 }  // namespace theory
 }  // namespace CVC5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__TERM_POOLS_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H */
diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h
index e6b577f4e..82f8e7698 100644
--- a/src/theory/quantifiers/term_registry.h
+++ b/src/theory/quantifiers/term_registry.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H
-#define CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TERM_REGISTRY_H
+#define CVC5__THEORY__QUANTIFIERS__TERM_REGISTRY_H
 
 #include <map>
 #include <unordered_set>
@@ -115,4 +115,4 @@ class TermRegistry
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__TERM_REGISTRY_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TERM_REGISTRY_H */
diff --git a/src/theory/quantifiers/term_tuple_enumerator.h b/src/theory/quantifiers/term_tuple_enumerator.h
index 4d6eb52f8..30ddde9c9 100644
--- a/src/theory/quantifiers/term_tuple_enumerator.h
+++ b/src/theory/quantifiers/term_tuple_enumerator.h
@@ -12,8 +12,8 @@
  ** \brief Implementation of an enumeration of tuples of terms for the purpose
  *of quantifier instantiation.
  **/
-#ifndef CVC4__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H
-#define CVC4__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__TERM_TUPLE_ENUMERATOR_H
 #include <vector>
 
 #include "expr/node.h"
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index d8a881e2e..96c3949f7 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H
-#define CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H
+#ifndef CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H
+#define CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H
 
 #include <map>
 
@@ -208,4 +208,4 @@ public:
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__TERM_UTIL_H */
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 716e8cdbd..2db7c393a 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
-#define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
+#ifndef CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
+#define CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H
 
 #include "expr/node.h"
 #include "theory/quantifiers/proof_checker.h"
@@ -102,4 +102,4 @@ class TheoryQuantifiers : public Theory {
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H */
diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index 53c077930..bafda3f88 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
-#define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
+#ifndef CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
+#define CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H
 
 #include "expr/node.h"
 #include "expr/type_node.h"
@@ -133,4 +133,4 @@ struct QuantifierInstPatternListTypeRule {
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H */