diff options
Diffstat (limited to 'src/theory/arrays/theory_arrays.cpp')
| -rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index d0a653410..29cd94c1d 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -788,8 +788,8 @@ void TheoryArrays::preRegisterTermInternal(TNode node) Assert(weakEquivGetRep(node) == node); d_infoMap.setWeakEquivPointer(node, node[0]); d_infoMap.setWeakEquivIndex(node, node[1]); -#ifdef CVC4_ASSERTIONS - checkWeakEquiv(false); +#ifdef CVC5_ASSERTIONS + checkWeakEquiv(false); #endif } @@ -867,7 +867,7 @@ void TheoryArrays::notifySharedTerm(TNode t) d_sharedArrays.insert(t); } else { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS d_sharedOther.insert(t); #endif d_sharedTerms = true; @@ -940,7 +940,7 @@ void TheoryArrays::checkPair(TNode r1, TNode r2) // Should have been propagated to us Assert(false); break; - case EQUALITY_FALSE: CVC4_FALLTHROUGH; + case EQUALITY_FALSE: CVC5_FALLTHROUGH; case EQUALITY_FALSE_IN_MODEL: // This is unlikely, but I think it could happen Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): checkPair called when false in model" << std::endl; @@ -1238,11 +1238,11 @@ void TheoryArrays::postCheck(Effort level) d_infoMap.setWeakEquivPointer(b, a); d_infoMap.setWeakEquivIndex(b, TNode()); } -#ifdef CVC4_ASSERTIONS - checkWeakEquiv(false); +#ifdef CVC5_ASSERTIONS + checkWeakEquiv(false); #endif } -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS checkWeakEquiv(true); #endif |