diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-09 17:22:07 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-09 17:22:07 -0700 |
| commit | f87f038c5f0821d0fefb01cea00bfdec6004da91 (patch) | |
| tree | d948178e1c0d2dc459a976f0d187d2d41a5437c0 /src/theory/strings | |
| parent | 550c49a7dd2b13ea29743458336f0c0a0fb6099a (diff) | |
Rename CVC4_ macros to CVC5_. (#6327)
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/arith_entail.cpp | 2 | ||||
| -rw-r--r-- | src/theory/strings/core_solver.cpp | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp index a1b2c487f..f98f6514e 100644 --- a/src/theory/strings/arith_entail.cpp +++ b/src/theory/strings/arith_entail.cpp @@ -174,7 +174,7 @@ bool ArithEntail::checkApprox(Node ar) { if (approxMsums.find(aa) == approxMsums.end()) { - CVC4_UNUSED bool ret = + CVC5_UNUSED bool ret = ArithMSum::getMonomialSum(aa, approxMsums[aa]); Assert(ret); } diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index f38acfac2..cfe80eea2 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -608,7 +608,7 @@ void CoreSolver::normalizeEquivalenceClass(Node eqc, TypeNode stype) Node emp = Word::mkEmptyWord(stype); if (d_state.areEqual(eqc, emp)) { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS for( unsigned j=0; j<d_eqc[eqc].size(); j++ ){ Node n = d_eqc[eqc][j]; for( unsigned i=0; i<n.getNumChildren(); i++ ){ |