Rename CVC4__ header guards to CVC5__. (#6326)

25 files changed, 69 insertions, 70 deletions

diff --git a/src/theory/bv/abstraction.h b/src/theory/bv/abstraction.h
index 182b29c19..be3b74d67 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__ABSTRACTION_H
-#define CVC4__THEORY__BV__ABSTRACTION_H
+#ifndef CVC5__THEORY__BV__ABSTRACTION_H
+#define CVC5__THEORY__BV__ABSTRACTION_H
 
 #include <unordered_map>
 #include <unordered_set>
diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
index 002ca71ec..2f4666a9b 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
-#define CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
+#ifndef CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
+#define CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
 
 #include "theory/bv/bitblast/bitblaster.h"
 
@@ -123,4 +123,4 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*>
 }  // namespace theory
 }  // namespace cvc5
 
-#endif  //  CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
+#endif  //  CVC5__THEORY__BV__BITBLAST__AIG_BITBLASTER_H
diff --git a/src/theory/bv/bitblast/bitblast_strategies_template.h b/src/theory/bv/bitblast/bitblast_strategies_template.h
index 72b079321..84d8faeb2 100644
--- a/src/theory/bv/bitblast/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast/bitblast_strategies_template.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
-#define CVC4__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
+#ifndef CVC5__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
+#define CVC5__THEORY__BV__BITBLAST__BITBLAST_STRATEGIES_TEMPLATE_H
 
 #include <cmath>
 #include <ostream>
diff --git a/src/theory/bv/bitblast/bitblast_utils.h b/src/theory/bv/bitblast/bitblast_utils.h
index 461d7fcaf..998e80c89 100644
--- a/src/theory/bv/bitblast/bitblast_utils.h
+++ b/src/theory/bv/bitblast/bitblast_utils.h
@@ -16,9 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
-#define CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
-
+#ifndef CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
+#define CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
 
 #include <ostream>
 #include "expr/node.h"
@@ -269,4 +268,4 @@ T inline sLessThanBB(const std::vector<T>&a, const std::vector<T>& b, bool orEqu
 }  // namespace theory
 }  // namespace cvc5
 
-#endif  // CVC4__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
+#endif  // CVC5__THEORY__BV__BITBLAST__BITBLAST_UTILS_H
diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index dd0be5cc0..b881537a8 100644
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
-#define CVC4__THEORY__BV__BITBLAST__BITBLASTER_H
+#ifndef CVC5__THEORY__BV__BITBLAST__BITBLASTER_H
+#define CVC5__THEORY__BV__BITBLAST__BITBLASTER_H
 
 #include <unordered_map>
 #include <unordered_set>
@@ -270,4 +270,4 @@ Node TBitblaster<T>::getTermModel(TNode node, bool fullModel)
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__BV__BITBLAST__BITBLASTER_H */
+#endif /* CVC5__THEORY__BV__BITBLAST__BITBLASTER_H */
diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h
index 87699df40..8ad13187c 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.h
+++ b/src/theory/bv/bitblast/eager_bitblaster.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
-#define CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+#ifndef CVC5__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+#define CVC5__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
 
 #include <memory>
 #include <unordered_set>
@@ -86,4 +86,4 @@ class BitblastingRegistrar : public prop::Registrar
 }  // namespace bv
 }  // namespace theory
 }  // namespace cvc5
-#endif  //  CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
+#endif  //  CVC5__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index 91995b56b..2a5f3425b 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
-#define CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+#ifndef CVC5__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+#define CVC5__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
 
 #include "theory/bv/bitblast/bitblaster.h"
 
@@ -177,4 +177,4 @@ class TLazyBitblaster : public TBitblaster<Node>
 }  // namespace bv
 }  // namespace theory
 }  // namespace cvc5
-#endif  //  CVC4__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
+#endif  //  CVC5__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h
index 4983b485e..dcd8e2737 100644
--- a/src/theory/bv/bitblast/proof_bitblaster.h
+++ b/src/theory/bv/bitblast/proof_bitblaster.h
@@ -13,8 +13,8 @@
  **/
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
-#define CVC4__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
+#ifndef CVC5__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
+#define CVC5__THEORY__BV__BITBLAST__PROOF_BITBLASTER_H
 
 #include "theory/bv/bitblast/simple_bitblaster.h"
 
diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h
index 300b93b53..7d78ed915 100644
--- a/src/theory/bv/bitblast/simple_bitblaster.h
+++ b/src/theory/bv/bitblast/simple_bitblaster.h
@@ -14,8 +14,8 @@
  **/
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
-#define CVC4__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
+#ifndef CVC5__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
+#define CVC5__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
 
 #include "theory/bv/bitblast/bitblaster.h"
 
diff --git a/src/theory/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 17e6c50e7..052023afb 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__BV_EAGER_SOLVER_H
-#define CVC4__THEORY__BV__BV_EAGER_SOLVER_H
+#ifndef CVC5__THEORY__BV__BV_EAGER_SOLVER_H
+#define CVC5__THEORY__BV__BV_EAGER_SOLVER_H
 
 #include "expr/node.h"
 #include "theory/bv/bv_solver_lazy.h"
@@ -62,4 +62,4 @@ class EagerBitblastSolver {
 }  // namespace theory
 }  // namespace cvc5
 
-#endif  // CVC4__THEORY__BV__BV_EAGER_SOLVER_H
+#endif  // CVC5__THEORY__BV__BV_EAGER_SOLVER_H
diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 3e856b789..e730c7c5a 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
-#define CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H
+#ifndef CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H
+#define CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H
 
 #include <queue>
 #include <unordered_map>
@@ -293,4 +293,4 @@ public:
 }
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__BV__BV_INEQUALITY__GRAPH_H */
+#endif /* CVC5__THEORY__BV__BV_INEQUALITY__GRAPH_H */
diff --git a/src/theory/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index 7dbd01dcd..685321bb1 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__BV_QUICK_CHECK_H
-#define CVC4__BV_QUICK_CHECK_H
+#ifndef CVC5__BV_QUICK_CHECK_H
+#define CVC5__BV_QUICK_CHECK_H
 
 #include <unordered_set>
 #include <vector>
@@ -183,4 +183,4 @@ class QuickXPlain
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__BV_QUICK_CHECK_H */
+#endif /* CVC5__BV_QUICK_CHECK_H */
diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h
index 8fa8fd850..1733f334b 100644
--- a/src/theory/bv/bv_solver.h
+++ b/src/theory/bv/bv_solver.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__BV_SOLVER_H
-#define CVC4__THEORY__BV__BV_SOLVER_H
+#ifndef CVC5__THEORY__BV__BV_SOLVER_H
+#define CVC5__THEORY__BV__BV_SOLVER_H
 
 #include "theory/theory.h"
 
@@ -119,4 +119,4 @@ class BVSolver
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__BV__BV_SOLVER_H */
+#endif /* CVC5__THEORY__BV__BV_SOLVER_H */
diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h
index 86a75e0aa..65c172964 100644
--- a/src/theory/bv/bv_solver_bitblast.h
+++ b/src/theory/bv/bv_solver_bitblast.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__BV_SOLVER_BITBLAST_H
-#define CVC4__THEORY__BV__BV_SOLVER_BITBLAST_H
+#ifndef CVC5__THEORY__BV__BV_SOLVER_BITBLAST_H
+#define CVC5__THEORY__BV__BV_SOLVER_BITBLAST_H
 
 #include <unordered_map>
 
diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h
index 35b9964e0..2689305e9 100644
--- a/src/theory/bv/bv_solver_lazy.h
+++ b/src/theory/bv/bv_solver_lazy.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__BV_SOLVER_LAZY_H
-#define CVC4__THEORY__BV__BV_SOLVER_LAZY_H
+#ifndef CVC5__THEORY__BV__BV_SOLVER_LAZY_H
+#define CVC5__THEORY__BV__BV_SOLVER_LAZY_H
 
 #include <unordered_map>
 #include <unordered_set>
@@ -231,4 +231,4 @@ class BVSolverLazy : public BVSolver
 
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__BV__BV_SOLVER_LAZY_H */
+#endif /* CVC5__THEORY__BV__BV_SOLVER_LAZY_H */
diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h
index 843032bef..1f805ee22 100644
--- a/src/theory/bv/bv_solver_simple.h
+++ b/src/theory/bv/bv_solver_simple.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
-#define CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H
+#ifndef CVC5__THEORY__BV__BV_SOLVER_SIMPLE_H
+#define CVC5__THEORY__BV__BV_SOLVER_SIMPLE_H
 
 #include "theory/bv/bitblast/proof_bitblaster.h"
 #include "theory/bv/bv_solver.h"
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index dec4614d3..323d1fbc6 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -14,8 +14,8 @@
  ** Interface for bit-vectors sub-solvers.
  **/
 
-#ifndef CVC4__THEORY__BV__BV_SUBTHEORY_H
-#define CVC4__THEORY__BV__BV_SUBTHEORY_H
+#ifndef CVC5__THEORY__BV__BV_SUBTHEORY_H
+#define CVC5__THEORY__BV__BV_SUBTHEORY_H
 
 #include "cvc4_private.h"
 #include "context/context.h"
@@ -109,4 +109,4 @@ class SubtheorySolver {
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__BV__BV_SUBTHEORY_H */
+#endif /* CVC5__THEORY__BV__BV_SUBTHEORY_H */
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index dc585b49b..4fe7d6bfe 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
-#define CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
+#ifndef CVC5__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
+#define CVC5__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H
 
 #include <unordered_set>
 
@@ -91,4 +91,4 @@ class InequalitySolver : public SubtheorySolver
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */
+#endif /* CVC5__THEORY__BV__BV_SUBTHEORY__INEQUALITY_H */
diff --git a/src/theory/bv/int_blaster.h b/src/theory/bv/int_blaster.h
index b76fc1cb7..22273a7f2 100644
--- a/src/theory/bv/int_blaster.h
+++ b/src/theory/bv/int_blaster.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__BV__INT_BLASTER__H
-#define __CVC4__THEORY__BV__INT_BLASTER__H
+#ifndef __CVC5__THEORY__BV__INT_BLASTER__H
+#define __CVC5__THEORY__BV__INT_BLASTER__H
 
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
@@ -351,4 +351,4 @@ class IntBlaster
 
 }  // namespace cvc5
 
-#endif /* __CVC4__THEORY__BV__INT_BLASTER_H */
+#endif /* __CVC5__THEORY__BV__INT_BLASTER_H */
diff --git a/src/theory/bv/proof_checker.h b/src/theory/bv/proof_checker.h
index b328600df..da696579f 100644
--- a/src/theory/bv/proof_checker.h
+++ b/src/theory/bv/proof_checker.h
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__PROOF_CHECKER_H
-#define CVC4__THEORY__BV__PROOF_CHECKER_H
+#ifndef CVC5__THEORY__BV__PROOF_CHECKER_H
+#define CVC5__THEORY__BV__PROOF_CHECKER_H
 
 #include "expr/node.h"
 #include "expr/proof_checker.h"
@@ -47,4 +47,4 @@ class BVProofRuleChecker : public ProofRuleChecker
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__BV__PROOF_CHECKER_H */
+#endif /* CVC5__THEORY__BV__PROOF_CHECKER_H */
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index 55a64d92b..b38df275c 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__SLICER_BV_H
-#define CVC4__THEORY__BV__SLICER_BV_H
+#ifndef CVC5__THEORY__BV__SLICER_BV_H
+#define CVC5__THEORY__BV__SLICER_BV_H
 
 #include <string>
 #include <vector>
@@ -53,4 +53,4 @@ public:
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__BV__SLICER_BV_H */
+#endif /* CVC5__THEORY__BV__SLICER_BV_H */
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 9176ef6ae..4a0c9dd53 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__THEORY_BV_H
-#define CVC4__THEORY__BV__THEORY_BV_H
+#ifndef CVC5__THEORY__BV__THEORY_BV_H
+#define CVC5__THEORY__BV__THEORY_BV_H
 
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/theory.h"
@@ -131,4 +131,4 @@ class TheoryBV : public Theory
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__BV__THEORY_BV_H */
+#endif /* CVC5__THEORY__BV__THEORY_BV_H */
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 0be333ef0..784168155 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__THEORY_BV_REWRITER_H
-#define CVC4__THEORY__BV__THEORY_BV_REWRITER_H
+#ifndef CVC5__THEORY__BV__THEORY_BV_REWRITER_H
+#define CVC5__THEORY__BV__THEORY_BV_REWRITER_H
 
 #include "theory/theory_rewriter.h"
 
@@ -107,4 +107,4 @@ class TheoryBVRewriter : public TheoryRewriter
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__BV__THEORY_BV_REWRITER_H */
+#endif /* CVC5__THEORY__BV__THEORY_BV_REWRITER_H */
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 4de7eed6d..fc85924ff 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -18,8 +18,8 @@
 
 #include <algorithm>
 
-#ifndef CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
-#define CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H
+#ifndef CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H
+#define CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H
 
 namespace cvc5 {
 namespace theory {
@@ -452,4 +452,4 @@ class BitVectorAckermanizationUremTypeRule
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__BV__THEORY_BV_TYPE_RULES_H */
+#endif /* CVC5__THEORY__BV__THEORY_BV_TYPE_RULES_H */
diff --git a/src/theory/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
index 826b61d6b..3451d0f61 100644
--- a/src/theory/bv/type_enumerator.h
+++ b/src/theory/bv/type_enumerator.h
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__BV__TYPE_ENUMERATOR_H
-#define CVC4__THEORY__BV__TYPE_ENUMERATOR_H
+#ifndef CVC5__THEORY__BV__TYPE_ENUMERATOR_H
+#define CVC5__THEORY__BV__TYPE_ENUMERATOR_H
 
 #include "expr/kind.h"
 #include "expr/type_node.h"
@@ -63,4 +63,4 @@ public:
 }  // namespace theory
 }  // namespace cvc5
 
-#endif /* CVC4__THEORY__BV__TYPE_ENUMERATOR_H */
+#endif /* CVC5__THEORY__BV__TYPE_ENUMERATOR_H */