diff options
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/array_info.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/inference_manager.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/proof_checker.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/skolem_cache.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/type_enumerator.h | 2 | ||||
-rw-r--r-- | src/theory/arrays/union_find.h | 2 |
9 files changed, 9 insertions, 9 deletions
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index 71033c77b..bbb9e8c62 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -14,7 +14,7 @@ * for each term of type array. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__ARRAY_INFO_H #define CVC5__THEORY__ARRAYS__ARRAY_INFO_H diff --git a/src/theory/arrays/inference_manager.h b/src/theory/arrays/inference_manager.h index b9809dbbb..93feb0a53 100644 --- a/src/theory/arrays/inference_manager.h +++ b/src/theory/arrays/inference_manager.h @@ -13,7 +13,7 @@ * Arrays inference manager. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__INFERENCE_MANAGER_H #define CVC5__THEORY__ARRAYS__INFERENCE_MANAGER_H diff --git a/src/theory/arrays/proof_checker.h b/src/theory/arrays/proof_checker.h index a3970baeb..9064dbfca 100644 --- a/src/theory/arrays/proof_checker.h +++ b/src/theory/arrays/proof_checker.h @@ -13,7 +13,7 @@ * Array proof checker utility. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__PROOF_CHECKER_H #define CVC5__THEORY__ARRAYS__PROOF_CHECKER_H diff --git a/src/theory/arrays/skolem_cache.h b/src/theory/arrays/skolem_cache.h index d4b774479..12578c01f 100644 --- a/src/theory/arrays/skolem_cache.h +++ b/src/theory/arrays/skolem_cache.h @@ -13,7 +13,7 @@ * Arrays skolem cache. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__SKOLEM_CACHE_H #define CVC5__THEORY__ARRAYS__SKOLEM_CACHE_H diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index af71f20f9..188573152 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -13,7 +13,7 @@ * Theory of arrays. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__THEORY_ARRAYS_H #define CVC5__THEORY__ARRAYS__THEORY_ARRAYS_H diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 3a0be799c..0bbfc0846 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -16,7 +16,7 @@ * \todo document this file */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H #define CVC5__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index 529cd2fb2..9a69ff8f4 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -13,7 +13,7 @@ * Typing and cardinality rules for the theory of arrays. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H #define CVC5__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h index 16b90730b..181a42da4 100644 --- a/src/theory/arrays/type_enumerator.h +++ b/src/theory/arrays/type_enumerator.h @@ -13,7 +13,7 @@ * An enumerator for arrays. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H #define CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h index b592eb307..c1a09491f 100644 --- a/src/theory/arrays/union_find.h +++ b/src/theory/arrays/union_find.h @@ -14,7 +14,7 @@ * stack. Refactored from the UF union-find. */ -#include "cvc4_private.h" +#include "cvc5_private.h" #ifndef CVC5__THEORY__ARRAYS__UNION_FIND_H #define CVC5__THEORY__ARRAYS__UNION_FIND_H |