diff options
Diffstat (limited to 'src/theory/strings/strings_rewriter.cpp')
-rw-r--r-- | src/theory/strings/strings_rewriter.cpp | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index 932b5c8cc..575c33501 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -251,15 +251,13 @@ Node StringsRewriter::rewriteStringLeq(Node n) { String s = n1[0].getConst<String>(); String t = n2[0].getConst<String>(); - // only need to truncate if s is longer - if (s.size() > t.size()) + size_t prefixLen = std::min(s.size(), t.size()); + s = s.prefix(prefixLen); + t = t.prefix(prefixLen); + // if the prefixes are not the same, then we can already decide the outcome + if (s != t) { - s = s.prefix(t.size()); - } - // if prefix is not leq, then entire string is not leq - if (!s.isLeq(t)) - { - Node ret = nm->mkConst(false); + Node ret = nm->mkConst(s.isLeq(t)); return returnRewrite(n, ret, Rewrite::STR_LEQ_CPREFIX); } } |