diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-02-14 02:52:14 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-02-14 02:52:14 -0800 |
| commit | dcd1b495c4500763fc4f453b1bad2341b5168d91 (patch) | |
| tree | 1e56655e7fb5f7d8895f8f5292caf278fe2e633a | |
| parent | d1e312cfe865bd7c167dff473f508f739d5ddc3b (diff) | |
Different not contains reduction
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index d095d6801..05b993a77 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -499,7 +499,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { NodeManager::currentNM()->mkNode( kind::LEQ, b1, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ) ), NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, x, b1, lens), s ) ); - retNode = NodeManager::currentNM()->mkNode( kind::EXISTS, b1v, body ); + retNode = nm->mkNode(kind::IMPLIES, nm->mkNode(kind::LEQ, lens, lenx), NodeManager::currentNM()->mkNode( kind::EXISTS, b1v, body )); } else if (t.getKind() == kind::STRING_LEQ) { |