diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-02-14 10:50:59 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-02-14 10:50:59 -0800 |
| commit | 908bf398a49ad8eefebee745eccf31a2f0f74ade (patch) | |
| tree | 76f8111a9bf018b5bc5738a885ee30767da12760 | |
| parent | 8912001d02be7bfdb8124781c3faf0de050f421c (diff) | |
alt versionnotCtnRed
| -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 e5cf00c8f..7afa7a9b0 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 = nm->mkNode(kind::AND, nm->mkNode(kind::LEQ, lens, lenx), NodeManager::currentNM()->mkNode( kind::EXISTS, b1v, body )); + retNode = nm->mkNode(kind::ITE, nm->mkNode(kind::LEQ, lens, lenx), NodeManager::currentNM()->mkNode( kind::EXISTS, b1v, body ), nm->mkConst(false)); } else if (t.getKind() == kind::STRING_LEQ) { |