diff options
Diffstat (limited to 'src/theory/strings/skolem_cache.cpp')
| -rw-r--r-- | src/theory/strings/skolem_cache.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 7396a5013..bdce86d06 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -15,7 +15,7 @@ #include "theory/strings/skolem_cache.h" #include "theory/rewriter.h" -#include "theory/strings/sequences_rewriter.h" +#include "theory/strings/arith_entail.h" #include "util/rational.h" using namespace CVC4::kind; @@ -163,8 +163,8 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b) a = s; b = m; } - else if (SequencesRewriter::checkEntailArith(nm->mkNode(PLUS, n, m), - nm->mkNode(STRING_LENGTH, s))) + else if (ArithEntail::check(nm->mkNode(PLUS, n, m), + nm->mkNode(STRING_LENGTH, s))) { // SK_PURIFY((str.substr x n m)) ---> SK_SUFFIX_REM(x, n) // if n + m >= (str.len x) |