diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-22 08:36:22 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-22 08:36:22 -0800 |
| commit | c8f205e9eafbb9b6df3c6624405b36dec5723c38 (patch) | |
| tree | acb08cbc0fc15b9f1b87c5a536f09d5c751dcc5e | |
| parent | 5b09e95f63e19940993b3301f1f7ceee62e2b2d5 (diff) | |
fix
| -rw-r--r-- | src/theory/strings/skolem_cache.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 6cf1606a8..7efedc310 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -122,7 +122,7 @@ SkolemCache::normalizeStringSkolem(SkolemId id, Node a, Node b, Node c) b = len; c = Node::null(); } - else if (c.getKind() != REGEXP_CONCAT) + else if (c == nm->mkNode(STRING_TO_REGEXP, nm->mkConst(String("")))) { id = SK_SUFFIX_REM; b = nm->mkNode(MINUS, nm->mkNode(STRING_LENGTH, a), len); |