Rename CVC4__ header guards to CVC5__. (#6326)

57 files changed, 169 insertions, 169 deletions

diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h
index 65385b0c4..49031e28a 100644
--- a/src/expr/array_store_all.h
+++ b/src/expr/array_store_all.h
@@ -18,8 +18,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef CVC4__ARRAY_STORE_ALL_H
-#define CVC4__ARRAY_STORE_ALL_H
+#ifndef CVC5__ARRAY_STORE_ALL_H
+#define CVC5__ARRAY_STORE_ALL_H
 
 #include <iosfwd>
 #include <memory>
@@ -71,4 +71,4 @@ struct ArrayStoreAllHashFunction
 
 }  // namespace cvc5
 
-#endif /* CVC4__ARRAY_STORE_ALL_H */
+#endif /* CVC5__ARRAY_STORE_ALL_H */
diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h
index b216a0fa1..fe6f2c23f 100644
--- a/src/expr/ascription_type.h
+++ b/src/expr/ascription_type.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef CVC4__ASCRIPTION_TYPE_H
-#define CVC4__ASCRIPTION_TYPE_H
+#ifndef CVC5__ASCRIPTION_TYPE_H
+#define CVC5__ASCRIPTION_TYPE_H
 
 #include <iosfwd>
 #include <memory>
@@ -62,4 +62,4 @@ std::ostream& operator<<(std::ostream& out, AscriptionType at);
 
 }  // namespace cvc5
 
-#endif /* CVC4__ASCRIPTION_TYPE_H */
+#endif /* CVC5__ASCRIPTION_TYPE_H */
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 6156ccc2d..9f2301d7e 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -21,8 +21,8 @@
 #include "expr/node.h"
 #include "expr/type_node.h"
 
-#ifndef CVC4__EXPR__ATTRIBUTE_H
-#define CVC4__EXPR__ATTRIBUTE_H
+#ifndef CVC5__EXPR__ATTRIBUTE_H
+#define CVC5__EXPR__ATTRIBUTE_H
 
 #include <string>
 #include "expr/attribute_unique_id.h"
@@ -623,4 +623,4 @@ NodeManager::setAttribute(TypeNode n, const AttrKind&,
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__ATTRIBUTE_H */
+#endif /* CVC5__EXPR__ATTRIBUTE_H */
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index db3e57675..2293e4b5a 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -20,8 +20,8 @@
 #  error expr/attribute_internals.h should only be included by expr/attribute.h
 #endif /* CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H */
 
-#ifndef CVC4__EXPR__ATTRIBUTE_INTERNALS_H
-#define CVC4__EXPR__ATTRIBUTE_INTERNALS_H
+#ifndef CVC5__EXPR__ATTRIBUTE_INTERNALS_H
+#define CVC5__EXPR__ATTRIBUTE_INTERNALS_H
 
 #include <unordered_map>
 
@@ -514,4 +514,4 @@ const uint64_t Attribute<T, bool, context_dep>::s_id =
 }  // namespace expr
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__ATTRIBUTE_INTERNALS_H */
+#endif /* CVC5__EXPR__ATTRIBUTE_INTERNALS_H */
diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h
index ebd107737..d1d1c1a38 100644
--- a/src/expr/bound_var_manager.h
+++ b/src/expr/bound_var_manager.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__BOUND_VAR_MANAGER_H
-#define CVC4__EXPR__BOUND_VAR_MANAGER_H
+#ifndef CVC5__EXPR__BOUND_VAR_MANAGER_H
+#define CVC5__EXPR__BOUND_VAR_MANAGER_H
 
 #include <string>
 #include <unordered_set>
@@ -100,4 +100,4 @@ class BoundVarManager
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__BOUND_VAR_MANAGER_H */
+#endif /* CVC5__EXPR__BOUND_VAR_MANAGER_H */
diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h
index 7399b3741..228af460c 100644
--- a/src/expr/buffered_proof_generator.h
+++ b/src/expr/buffered_proof_generator.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H
-#define CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H
+#ifndef CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H
+#define CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H
 
 #include "context/cdhashmap.h"
 #include "expr/proof_generator.h"
@@ -59,4 +59,4 @@ class BufferedProofGenerator : public ProofGenerator
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H */
+#endif /* CVC5__EXPR__BUFFERED_PROOF_GENERATOR_H */
diff --git a/src/expr/datatype_index.h b/src/expr/datatype_index.h
index a239c387b..ca4d6d743 100644
--- a/src/expr/datatype_index.h
+++ b/src/expr/datatype_index.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef CVC4__DATATYPE_INDEX_H
-#define CVC4__DATATYPE_INDEX_H
+#ifndef CVC5__DATATYPE_INDEX_H
+#define CVC5__DATATYPE_INDEX_H
 
 #include <iosfwd>
 
@@ -66,4 +66,4 @@ struct DatatypeIndexConstantHashFunction
 
 }  // namespace cvc5
 
-#endif /* CVC4__DATATYPE_H */
+#endif /* CVC5__DATATYPE_H */
diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index 524702bdd..e0f37d811 100644
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__DTYPE_H
-#define CVC4__EXPR__DTYPE_H
+#ifndef CVC5__EXPR__DTYPE_H
+#define CVC5__EXPR__DTYPE_H
 
 #include <map>
 #include <string>
diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h
index d444d9261..52b0a4d69 100644
--- a/src/expr/dtype_cons.h
+++ b/src/expr/dtype_cons.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__DTYPE_CONS_H
-#define CVC4__EXPR__DTYPE_CONS_H
+#ifndef CVC5__EXPR__DTYPE_CONS_H
+#define CVC5__EXPR__DTYPE_CONS_H
 
 #include <map>
 #include <string>
diff --git a/src/expr/dtype_selector.h b/src/expr/dtype_selector.h
index d45bcf8c5..66a4f4f4f 100644
--- a/src/expr/dtype_selector.h
+++ b/src/expr/dtype_selector.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__DTYPE_SELECTOR_H
-#define CVC4__EXPR__DTYPE_SELECTOR_H
+#ifndef CVC5__EXPR__DTYPE_SELECTOR_H
+#define CVC5__EXPR__DTYPE_SELECTOR_H
 
 #include <string>
 #include "expr/node.h"
diff --git a/src/expr/emptybag.h b/src/expr/emptybag.h
index f45bd9e96..19efe3a94 100644
--- a/src/expr/emptybag.h
+++ b/src/expr/emptybag.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef CVC4__EMPTY_BAG_H
-#define CVC4__EMPTY_BAG_H
+#ifndef CVC5__EMPTY_BAG_H
+#define CVC5__EMPTY_BAG_H
 
 #include <iosfwd>
 #include <memory>
@@ -60,4 +60,4 @@ struct EmptyBagHashFunction
 
 }  // namespace cvc5
 
-#endif /* CVC4__EMPTY_BAG_H */
+#endif /* CVC5__EMPTY_BAG_H */
diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h
index aa6d5e143..b1c00a5ad 100644
--- a/src/expr/emptyset.h
+++ b/src/expr/emptyset.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef CVC4__EMPTY_SET_H
-#define CVC4__EMPTY_SET_H
+#ifndef CVC5__EMPTY_SET_H
+#define CVC5__EMPTY_SET_H
 
 #include <iosfwd>
 #include <memory>
@@ -62,4 +62,4 @@ struct EmptySetHashFunction
 
 }  // namespace cvc5
 
-#endif /* CVC4__EMPTY_SET_H */
+#endif /* CVC5__EMPTY_SET_H */
diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h
index 674d4c6fd..91b0fcc2e 100644
--- a/src/expr/expr_iomanip.h
+++ b/src/expr/expr_iomanip.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef CVC4__EXPR__EXPR_IOMANIP_H
-#define CVC4__EXPR__EXPR_IOMANIP_H
+#ifndef CVC5__EXPR__EXPR_IOMANIP_H
+#define CVC5__EXPR__EXPR_IOMANIP_H
 
 #include <iosfwd>
 
@@ -175,4 +175,4 @@ std::ostream& operator<<(std::ostream& out, ExprSetDepth sd);
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__EXPR_IOMANIP_H */
+#endif /* CVC5__EXPR__EXPR_IOMANIP_H */
diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h
index 0716ff4d0..28cbf5c37 100644
--- a/src/expr/kind_map.h
+++ b/src/expr/kind_map.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__KIND_MAP_H
-#define CVC4__KIND_MAP_H
+#ifndef CVC5__KIND_MAP_H
+#define CVC5__KIND_MAP_H
 
 #include <bitset>
 
@@ -53,4 +53,4 @@ class KindMap
 
 }  // namespace cvc5
 
-#endif /* CVC4__KIND_MAP_H */
+#endif /* CVC5__KIND_MAP_H */
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 484e8c273..d24f46551 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef CVC4__KIND_H
-#define CVC4__KIND_H
+#ifndef CVC5__KIND_H
+#define CVC5__KIND_H
 
 #include <iosfwd>
 
@@ -104,4 +104,4 @@ namespace theory {
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__KIND_H */
+#endif /* CVC5__KIND_H */
diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h
index 3ab0ca49e..b60bfd409 100644
--- a/src/expr/lazy_proof.h
+++ b/src/expr/lazy_proof.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__LAZY_PROOF_H
-#define CVC4__EXPR__LAZY_PROOF_H
+#ifndef CVC5__EXPR__LAZY_PROOF_H
+#define CVC5__EXPR__LAZY_PROOF_H
 
 #include "expr/proof.h"
 
@@ -107,4 +107,4 @@ class LazyCDProof : public CDProof
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__LAZY_PROOF_H */
+#endif /* CVC5__EXPR__LAZY_PROOF_H */
diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h
index 41488c821..87881fae1 100644
--- a/src/expr/lazy_proof_chain.h
+++ b/src/expr/lazy_proof_chain.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__LAZY_PROOF_CHAIN_H
-#define CVC4__EXPR__LAZY_PROOF_CHAIN_H
+#ifndef CVC5__EXPR__LAZY_PROOF_CHAIN_H
+#define CVC5__EXPR__LAZY_PROOF_CHAIN_H
 
 #include <vector>
 
@@ -150,4 +150,4 @@ class LazyCDProofChain : public ProofGenerator
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__LAZY_PROOF_CHAIN_H */
+#endif /* CVC5__EXPR__LAZY_PROOF_CHAIN_H */
diff --git a/src/expr/match_trie.h b/src/expr/match_trie.h
index 70ce549e1..6f85d20c9 100644
--- a/src/expr/match_trie.h
+++ b/src/expr/match_trie.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__MATCH_TRIE_H
-#define CVC4__EXPR__MATCH_TRIE_H
+#ifndef CVC5__EXPR__MATCH_TRIE_H
+#define CVC5__EXPR__MATCH_TRIE_H
 
 #include <map>
 #include <vector>
@@ -79,4 +79,4 @@ class MatchTrie
 }  // namespace expr
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */
+#endif /* CVC5__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 5c78d87d3..7f232b4e2 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__KIND__METAKIND_H
-#define CVC4__KIND__METAKIND_H
+#ifndef CVC5__KIND__METAKIND_H
+#define CVC5__KIND__METAKIND_H
 
 #include <iosfwd>
 
@@ -128,11 +128,11 @@ struct NodeValuePoolEq {
 
 #include "expr/node_value.h"
 
-#endif /* CVC4__KIND__METAKIND_H */
+#endif /* CVC5__KIND__METAKIND_H */
 
 ${metakind_includes}
 
-#ifdef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
+#ifdef CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP
 
 namespace cvc5 {
 
@@ -207,4 +207,4 @@ Kind operatorToKind(::cvc5::expr::NodeValue* nv);
 
 }  // namespace cvc5
 
-#endif /* CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */
+#endif /* CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP */
diff --git a/src/expr/node.h b/src/expr/node.h
index fb3cf1478..b8e44a4cb 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -19,8 +19,8 @@
 // circular dependency
 #include "expr/node_value.h"
 
-#ifndef CVC4__NODE_H
-#define CVC4__NODE_H
+#ifndef CVC5__NODE_H
+#define CVC5__NODE_H
 
 #include <iostream>
 #include <map>
@@ -1492,4 +1492,4 @@ static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>&
 
 }  // namespace cvc5
 
-#endif /* CVC4__NODE_H */
+#endif /* CVC5__NODE_H */
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index 7ae56e5ba..09630cb28 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__NODE_ALGORITHM_H
-#define CVC4__EXPR__NODE_ALGORITHM_H
+#ifndef CVC5__EXPR__NODE_ALGORITHM_H
+#define CVC5__EXPR__NODE_ALGORITHM_H
 
 #include <unordered_map>
 #include <vector>
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 218a08766..271a217dc 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -137,8 +137,8 @@
 /* strong dependency; make sure node is included first */
 #include "expr/node.h"
 
-#ifndef CVC4__NODE_BUILDER_H
-#define CVC4__NODE_BUILDER_H
+#ifndef CVC5__NODE_BUILDER_H
+#define CVC5__NODE_BUILDER_H
 
 #include <iostream>
 #include <vector>
@@ -407,4 +407,4 @@ std::ostream& operator<<(std::ostream& out, const NodeBuilder& nb);
 
 }  // namespace cvc5
 
-#endif /* CVC4__NODE_BUILDER_H */
+#endif /* CVC5__NODE_BUILDER_H */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 465ddf588..98eb111bc 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -23,8 +23,8 @@
 #include "expr/node.h"
 #include "expr/type_node.h"
 
-#ifndef CVC4__NODE_MANAGER_H
-#define CVC4__NODE_MANAGER_H
+#ifndef CVC5__NODE_MANAGER_H
+#define CVC5__NODE_MANAGER_H
 
 #include <vector>
 #include <string>
@@ -1197,9 +1197,9 @@ inline void NodeManager::poolRemove(expr::NodeValue* nv) {
 
 }  // namespace cvc5
 
-#define CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
+#define CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP
 #include "expr/metakind.h"
-#undef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
+#undef CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP
 
 #include "expr/node_builder.h"
 
@@ -1572,4 +1572,4 @@ NodeClass NodeManager::mkConstInternal(const T& val) {
 
 }  // namespace cvc5
 
-#endif /* CVC4__NODE_MANAGER_H */
+#endif /* CVC5__NODE_MANAGER_H */
diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h
index d8558de97..73fecf4ef 100644
--- a/src/expr/node_self_iterator.h
+++ b/src/expr/node_self_iterator.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__NODE_SELF_ITERATOR_H
-#define CVC4__EXPR__NODE_SELF_ITERATOR_H
+#ifndef CVC5__EXPR__NODE_SELF_ITERATOR_H
+#define CVC5__EXPR__NODE_SELF_ITERATOR_H
 
 #include <iterator>
 
@@ -125,4 +125,4 @@ inline bool NodeSelfIterator::operator!=(NodeSelfIterator i) const {
 }  // namespace expr
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__NODE_SELF_ITERATOR_H */
+#endif /* CVC5__EXPR__NODE_SELF_ITERATOR_H */
diff --git a/src/expr/node_traversal.h b/src/expr/node_traversal.h
index 015bcec06..4b695d2ba 100644
--- a/src/expr/node_traversal.h
+++ b/src/expr/node_traversal.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__NODE_TRAVERSAL_H
-#define CVC4__EXPR__NODE_TRAVERSAL_H
+#ifndef CVC5__EXPR__NODE_TRAVERSAL_H
+#define CVC5__EXPR__NODE_TRAVERSAL_H
 
 #include <iterator>
 #include <unordered_map>
@@ -146,4 +146,4 @@ class NodeDfsIterable
 
 }  // namespace cvc5
 
-#endif  // CVC4__EXPR__NODE_TRAVERSAL_H
+#endif  // CVC5__EXPR__NODE_TRAVERSAL_H
diff --git a/src/expr/node_trie.h b/src/expr/node_trie.h
index 2f42b6a52..c2c686295 100644
--- a/src/expr/node_trie.h
+++ b/src/expr/node_trie.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__NODE_TRIE_H
-#define CVC4__EXPR__NODE_TRIE_H
+#ifndef CVC5__EXPR__NODE_TRIE_H
+#define CVC5__EXPR__NODE_TRIE_H
 
 #include <map>
 #include "expr/node.h"
@@ -109,4 +109,4 @@ typedef NodeTemplateTrie<false> TNodeTrie;
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__NODE_TRIE_H */
+#endif /* CVC5__EXPR__NODE_TRIE_H */
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 3f4b7602e..3e1ccd67e 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -23,8 +23,8 @@
 // circular dependency
 #include "expr/metakind.h"
 
-#ifndef CVC4__EXPR__NODE_VALUE_H
-#define CVC4__EXPR__NODE_VALUE_H
+#ifndef CVC5__EXPR__NODE_VALUE_H
+#define CVC5__EXPR__NODE_VALUE_H
 
 #include <iterator>
 #include <string>
@@ -546,4 +546,4 @@ static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue*
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__NODE_VALUE_H */
+#endif /* CVC5__EXPR__NODE_VALUE_H */
diff --git a/src/expr/proof.h b/src/expr/proof.h
index af859df93..5cea5354e 100644
--- a/src/expr/proof.h
+++ b/src/expr/proof.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__PROOF_H
-#define CVC4__EXPR__PROOF_H
+#ifndef CVC5__EXPR__PROOF_H
+#define CVC5__EXPR__PROOF_H
 
 #include <vector>
 
@@ -275,4 +275,4 @@ class CDProof : public ProofGenerator
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__PROOF_MANAGER_H */
+#endif /* CVC5__EXPR__PROOF_MANAGER_H */
diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h
index 99f9f3ec8..06e813e2d 100644
--- a/src/expr/proof_checker.h
+++ b/src/expr/proof_checker.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__PROOF_CHECKER_H
-#define CVC4__EXPR__PROOF_CHECKER_H
+#ifndef CVC5__EXPR__PROOF_CHECKER_H
+#define CVC5__EXPR__PROOF_CHECKER_H
 
 #include <map>
 
@@ -204,4 +204,4 @@ class ProofChecker
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__PROOF_CHECKER_H */
+#endif /* CVC5__EXPR__PROOF_CHECKER_H */
diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h
index d610147d4..8a7461287 100644
--- a/src/expr/proof_ensure_closed.h
+++ b/src/expr/proof_ensure_closed.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__PROOF_ENSURE_CLOSED_H
-#define CVC4__EXPR__PROOF_ENSURE_CLOSED_H
+#ifndef CVC5__EXPR__PROOF_ENSURE_CLOSED_H
+#define CVC5__EXPR__PROOF_ENSURE_CLOSED_H
 
 #include "expr/node.h"
 
@@ -69,4 +69,4 @@ void pfnEnsureClosedWrt(ProofNode* pn,
                         const char* ctx);
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__PROOF_ENSURE_CLOSED_H */
+#endif /* CVC5__EXPR__PROOF_ENSURE_CLOSED_H */
diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h
index 76a2c9b3b..2cc64e083 100644
--- a/src/expr/proof_generator.h
+++ b/src/expr/proof_generator.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__PROOF_GENERATOR_H
-#define CVC4__EXPR__PROOF_GENERATOR_H
+#ifndef CVC5__EXPR__PROOF_GENERATOR_H
+#define CVC5__EXPR__PROOF_GENERATOR_H
 
 #include "expr/node.h"
 
@@ -109,4 +109,4 @@ class ProofGenerator
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__PROOF_GENERATOR_H */
+#endif /* CVC5__EXPR__PROOF_GENERATOR_H */
diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h
index ddd8e1e27..b849e2391 100644
--- a/src/expr/proof_node.h
+++ b/src/expr/proof_node.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__PROOF_NODE_H
-#define CVC4__EXPR__PROOF_NODE_H
+#ifndef CVC5__EXPR__PROOF_NODE_H
+#define CVC5__EXPR__PROOF_NODE_H
 
 #include <vector>
 
@@ -141,4 +141,4 @@ std::ostream& operator<<(std::ostream& out, const ProofNode& pn);
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__PROOF_NODE_H */
+#endif /* CVC5__EXPR__PROOF_NODE_H */
diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h
index 01faa8a40..6aa045481 100644
--- a/src/expr/proof_node_algorithm.h
+++ b/src/expr/proof_node_algorithm.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__PROOF_NODE_ALGORITHM_H
-#define CVC4__EXPR__PROOF_NODE_ALGORITHM_H
+#ifndef CVC5__EXPR__PROOF_NODE_ALGORITHM_H
+#define CVC5__EXPR__PROOF_NODE_ALGORITHM_H
 
 #include <vector>
 
@@ -72,4 +72,4 @@ bool containsSubproof(ProofNode* pn,
 }  // namespace expr
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__PROOF_NODE_ALGORITHM_H */
+#endif /* CVC5__EXPR__PROOF_NODE_ALGORITHM_H */
diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
index 32513cd0d..251d43ed3 100644
--- a/src/expr/proof_node_manager.h
+++ b/src/expr/proof_node_manager.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__PROOF_NODE_MANAGER_H
-#define CVC4__EXPR__PROOF_NODE_MANAGER_H
+#ifndef CVC5__EXPR__PROOF_NODE_MANAGER_H
+#define CVC5__EXPR__PROOF_NODE_MANAGER_H
 
 #include <vector>
 
@@ -202,4 +202,4 @@ class ProofNodeManager
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__PROOF_NODE_H */
+#endif /* CVC5__EXPR__PROOF_NODE_H */
diff --git a/src/expr/proof_node_to_sexpr.h b/src/expr/proof_node_to_sexpr.h
index bbbde39f6..31b04466e 100644
--- a/src/expr/proof_node_to_sexpr.h
+++ b/src/expr/proof_node_to_sexpr.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__PROOF_NODE_TO_SEXPR_H
-#define CVC4__EXPR__PROOF_NODE_TO_SEXPR_H
+#ifndef CVC5__EXPR__PROOF_NODE_TO_SEXPR_H
+#define CVC5__EXPR__PROOF_NODE_TO_SEXPR_H
 
 #include <map>
 
@@ -66,4 +66,4 @@ class ProofNodeToSExpr
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__PROOF_RULE_H */
+#endif /* CVC5__EXPR__PROOF_RULE_H */
diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h
index 268fcda5e..6f3e5b420 100644
--- a/src/expr/proof_node_updater.h
+++ b/src/expr/proof_node_updater.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__PROOF_NODE_UPDATER_H
-#define CVC4__EXPR__PROOF_NODE_UPDATER_H
+#ifndef CVC5__EXPR__PROOF_NODE_UPDATER_H
+#define CVC5__EXPR__PROOF_NODE_UPDATER_H
 
 #include <map>
 #include <memory>
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index cec85cc99..8aaf697d4 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__PROOF_RULE_H
-#define CVC4__EXPR__PROOF_RULE_H
+#ifndef CVC5__EXPR__PROOF_RULE_H
+#define CVC5__EXPR__PROOF_RULE_H
 
 #include <iosfwd>
 
@@ -1385,4 +1385,4 @@ struct PfRuleHashFunction
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__PROOF_RULE_H */
+#endif /* CVC5__EXPR__PROOF_RULE_H */
diff --git a/src/expr/proof_set.h b/src/expr/proof_set.h
index 0509ed9d4..f684045c6 100644
--- a/src/expr/proof_set.h
+++ b/src/expr/proof_set.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__PROOF_SET_H
-#define CVC4__EXPR__PROOF_SET_H
+#ifndef CVC5__EXPR__PROOF_SET_H
+#define CVC5__EXPR__PROOF_SET_H
 
 #include <memory>
 
@@ -72,4 +72,4 @@ class CDProofSet
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__LAZY_PROOF_SET_H */
+#endif /* CVC5__EXPR__LAZY_PROOF_SET_H */
diff --git a/src/expr/proof_step_buffer.h b/src/expr/proof_step_buffer.h
index 99a7608ff..ef57540c7 100644
--- a/src/expr/proof_step_buffer.h
+++ b/src/expr/proof_step_buffer.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__PROOF_STEP_BUFFER_H
-#define CVC4__EXPR__PROOF_STEP_BUFFER_H
+#ifndef CVC5__EXPR__PROOF_STEP_BUFFER_H
+#define CVC5__EXPR__PROOF_STEP_BUFFER_H
 
 #include <vector>
 
@@ -94,4 +94,4 @@ class ProofStepBuffer
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__PROOF_STEP_BUFFER_H */
+#endif /* CVC5__EXPR__PROOF_STEP_BUFFER_H */
diff --git a/src/expr/record.h b/src/expr/record.h
index 436b5b269..fa6a34395 100644
--- a/src/expr/record.h
+++ b/src/expr/record.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef CVC4__RECORD_H
-#define CVC4__RECORD_H
+#ifndef CVC5__RECORD_H
+#define CVC5__RECORD_H
 
 #include <iostream>
 #include <string>
@@ -58,4 +58,4 @@ using Record = std::vector<std::pair<std::string, TypeNode>>;
 
 }  // namespace cvc5
 
-#endif /* CVC4__RECORD_H */
+#endif /* CVC5__RECORD_H */
diff --git a/src/expr/sequence.h b/src/expr/sequence.h
index e42851f58..e75c38956 100644
--- a/src/expr/sequence.h
+++ b/src/expr/sequence.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef CVC4__EXPR__SEQUENCE_H
-#define CVC4__EXPR__SEQUENCE_H
+#ifndef CVC5__EXPR__SEQUENCE_H
+#define CVC5__EXPR__SEQUENCE_H
 
 #include <memory>
 #include <vector>
@@ -175,4 +175,4 @@ std::ostream& operator<<(std::ostream& os, const Sequence& s);
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__SEQUENCE_H */
+#endif /* CVC5__EXPR__SEQUENCE_H */
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 6cebee5d9..b69853a85 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__SKOLEM_MANAGER_H
-#define CVC4__EXPR__SKOLEM_MANAGER_H
+#ifndef CVC5__EXPR__SKOLEM_MANAGER_H
+#define CVC5__EXPR__SKOLEM_MANAGER_H
 
 #include <string>
 
@@ -314,4 +314,4 @@ class SkolemManager
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__PROOF_SKOLEM_CACHE_H */
+#endif /* CVC5__EXPR__PROOF_SKOLEM_CACHE_H */
diff --git a/src/expr/subs.h b/src/expr/subs.h
index fdb8e4551..d351eeaa7 100644
--- a/src/expr/subs.h
+++ b/src/expr/subs.h
@@ -12,8 +12,8 @@
  ** \brief Simple substitution utility
  **/
 
-#ifndef CVC4__EXPR__SUBS_H
-#define CVC4__EXPR__SUBS_H
+#ifndef CVC5__EXPR__SUBS_H
+#define CVC5__EXPR__SUBS_H
 
 #include <map>
 #include <vector>
@@ -82,4 +82,4 @@ std::ostream& operator<<(std::ostream& out, const Subs& s);
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__SUBS_H */
+#endif /* CVC5__EXPR__SUBS_H */
diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h
index e5d1de740..b3130a028 100644
--- a/src/expr/sygus_datatype.h
+++ b/src/expr/sygus_datatype.h
@@ -13,8 +13,8 @@
  **/
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__SYGUS_DATATYPE_H
-#define CVC4__EXPR__SYGUS_DATATYPE_H
+#ifndef CVC5__EXPR__SYGUS_DATATYPE_H
+#define CVC5__EXPR__SYGUS_DATATYPE_H
 
 #include <string>
 #include <vector>
diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h
index 4ff307bc2..96bc3954d 100644
--- a/src/expr/symbol_manager.h
+++ b/src/expr/symbol_manager.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef CVC4__EXPR__SYMBOL_MANAGER_H
-#define CVC4__EXPR__SYMBOL_MANAGER_H
+#ifndef CVC5__EXPR__SYMBOL_MANAGER_H
+#define CVC5__EXPR__SYMBOL_MANAGER_H
 
 #include <map>
 #include <memory>
@@ -158,4 +158,4 @@ class CVC4_EXPORT SymbolManager
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__SYMBOL_MANAGER_H */
+#endif /* CVC5__EXPR__SYMBOL_MANAGER_H */
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index fbb1969dd..98cba9ff8 100644
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef CVC4__SYMBOL_TABLE_H
-#define CVC4__SYMBOL_TABLE_H
+#ifndef CVC5__SYMBOL_TABLE_H
+#define CVC5__SYMBOL_TABLE_H
 
 #include <memory>
 #include <string>
@@ -212,4 +212,4 @@ class CVC4_EXPORT SymbolTable
 
 }  // namespace cvc5
 
-#endif /* CVC4__SYMBOL_TABLE_H */
+#endif /* CVC5__SYMBOL_TABLE_H */
diff --git a/src/expr/tconv_seq_proof_generator.h b/src/expr/tconv_seq_proof_generator.h
index 151cd511d..2e14acb98 100644
--- a/src/expr/tconv_seq_proof_generator.h
+++ b/src/expr/tconv_seq_proof_generator.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H
-#define CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H
+#ifndef CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H
+#define CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H
 
 #include "context/cdhashmap.h"
 #include "expr/node.h"
@@ -117,4 +117,4 @@ class TConvSeqProofGenerator : public ProofGenerator
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__TCONV_SEQ_PROOF_GENERATOR_H */
+#endif /* CVC5__EXPR__TCONV_SEQ_PROOF_GENERATOR_H */
diff --git a/src/expr/term_canonize.h b/src/expr/term_canonize.h
index f15bb2df0..a032f3a84 100644
--- a/src/expr/term_canonize.h
+++ b/src/expr/term_canonize.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__TERM_CANONIZE_H
-#define CVC4__EXPR__TERM_CANONIZE_H
+#ifndef CVC5__EXPR__TERM_CANONIZE_H
+#define CVC5__EXPR__TERM_CANONIZE_H
 
 #include <map>
 #include "expr/node.h"
@@ -102,4 +102,4 @@ class TermCanonize
 }  // namespace expr
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__TERM_CANONIZE_H */
+#endif /* CVC5__EXPR__TERM_CANONIZE_H */
diff --git a/src/expr/term_context.h b/src/expr/term_context.h
index 062104fc2..5bdab4fca 100644
--- a/src/expr/term_context.h
+++ b/src/expr/term_context.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__TERM_CONTEXT_H
-#define CVC4__EXPR__TERM_CONTEXT_H
+#ifndef CVC5__EXPR__TERM_CONTEXT_H
+#define CVC5__EXPR__TERM_CONTEXT_H
 
 #include "expr/node.h"
 
@@ -165,4 +165,4 @@ class PolarityTermContext : public TermContext
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */
+#endif /* CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */
diff --git a/src/expr/term_context_node.h b/src/expr/term_context_node.h
index 5af435a56..1c3542b57 100644
--- a/src/expr/term_context_node.h
+++ b/src/expr/term_context_node.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__TERM_CONTEXT_NODE_H
-#define CVC4__EXPR__TERM_CONTEXT_NODE_H
+#ifndef CVC5__EXPR__TERM_CONTEXT_NODE_H
+#define CVC5__EXPR__TERM_CONTEXT_NODE_H
 
 #include "expr/node.h"
 
@@ -76,4 +76,4 @@ class TCtxNode
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */
+#endif /* CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */
diff --git a/src/expr/term_context_stack.h b/src/expr/term_context_stack.h
index 0042091ed..48892e654 100644
--- a/src/expr/term_context_stack.h
+++ b/src/expr/term_context_stack.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__TERM_CONTEXT_STACK_H
-#define CVC4__EXPR__TERM_CONTEXT_STACK_H
+#ifndef CVC5__EXPR__TERM_CONTEXT_STACK_H
+#define CVC5__EXPR__TERM_CONTEXT_STACK_H
 
 #include "expr/term_context_node.h"
 
@@ -70,4 +70,4 @@ class TCtxStack
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__TERM_CONTEXT_STACK_H */
+#endif /* CVC5__EXPR__TERM_CONTEXT_STACK_H */
diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h
index e1f2b90e8..961ac61cc 100644
--- a/src/expr/term_conversion_proof_generator.h
+++ b/src/expr/term_conversion_proof_generator.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H
-#define CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H
+#ifndef CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H
+#define CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H
 
 #include "context/cdhashmap.h"
 #include "expr/lazy_proof.h"
@@ -244,4 +244,4 @@ class TConvProofGenerator : public ProofGenerator
 
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */
+#endif /* CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */
diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h
index fee02de75..5b806e671 100644
--- a/src/expr/type_checker.h
+++ b/src/expr/type_checker.h
@@ -19,8 +19,8 @@
 // ordering dependence
 #include "expr/node.h"
 
-#ifndef CVC4__EXPR__TYPE_CHECKER_H
-#define CVC4__EXPR__TYPE_CHECKER_H
+#ifndef CVC5__EXPR__TYPE_CHECKER_H
+#define CVC5__EXPR__TYPE_CHECKER_H
 
 namespace cvc5 {
 namespace expr {
@@ -38,4 +38,4 @@ public:
 }  // namespace expr
 }  // namespace cvc5
 
-#endif /* CVC4__EXPR__TYPE_CHECKER_H */
+#endif /* CVC5__EXPR__TYPE_CHECKER_H */
diff --git a/src/expr/type_matcher.h b/src/expr/type_matcher.h
index a75bb7b8b..6df955c06 100644
--- a/src/expr/type_matcher.h
+++ b/src/expr/type_matcher.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__EXPR__TYPE_MATCHER_H
-#define CVC4__EXPR__TYPE_MATCHER_H
+#ifndef CVC5__EXPR__TYPE_MATCHER_H
+#define CVC5__EXPR__TYPE_MATCHER_H
 
 #include <vector>
 
@@ -70,4 +70,4 @@ class TypeMatcher
 
 }  // namespace cvc5
 
-#endif /* CVC4__MATCHER_H */
+#endif /* CVC5__MATCHER_H */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index f8cc5a44b..41f9afe6f 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -19,8 +19,8 @@
 // circular dependency
 #include "expr/node_value.h"
 
-#ifndef CVC4__TYPE_NODE_H
-#define CVC4__TYPE_NODE_H
+#ifndef CVC5__TYPE_NODE_H
+#define CVC5__TYPE_NODE_H
 
 #include <iostream>
 #include <string>
@@ -1070,4 +1070,4 @@ static void __attribute__((used)) debugPrintRawTypeNode(const TypeNode& n) {
 
 }  // namespace cvc5
 
-#endif /* CVC4__NODE_H */
+#endif /* CVC5__NODE_H */
diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h
index ce2696c5b..c6fb29b71 100644
--- a/src/expr/type_properties_template.h
+++ b/src/expr/type_properties_template.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__TYPE_PROPERTIES_H
-#define CVC4__TYPE_PROPERTIES_H
+#ifndef CVC5__TYPE_PROPERTIES_H
+#define CVC5__TYPE_PROPERTIES_H
 
 #include <sstream>
 
@@ -116,4 +116,4 @@ ${type_groundterms}
 }  // namespace kind
 }  // namespace cvc5
 
-#endif /* CVC4__TYPE_PROPERTIES_H */
+#endif /* CVC5__TYPE_PROPERTIES_H */
diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h
index 94d7f85ed..841b32626 100644
--- a/src/expr/uninterpreted_constant.h
+++ b/src/expr/uninterpreted_constant.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef CVC4__UNINTERPRETED_CONSTANT_H
-#define CVC4__UNINTERPRETED_CONSTANT_H
+#ifndef CVC5__UNINTERPRETED_CONSTANT_H
+#define CVC5__UNINTERPRETED_CONSTANT_H
 
 #include <iosfwd>
 #include <memory>
@@ -62,4 +62,4 @@ struct UninterpretedConstantHashFunction
 
 }  // namespace cvc5
 
-#endif /* CVC4__UNINTERPRETED_CONSTANT_H */
+#endif /* CVC5__UNINTERPRETED_CONSTANT_H */