diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-06-21 16:25:12 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-06-21 16:25:12 -0700 |
| commit | ffb3f16b0b13157dacdefecdb28bf8ab94e37b40 (patch) | |
| tree | 76ad3efedffccfe7b6161742a4f50d3316093241 | |
| parent | 4a5d9b2a24734390b2e04a1c9b23e3c89b396525 (diff) | |
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 3ffccbf48..3a261376b 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -218,11 +218,6 @@ void RegExpSolver::check() } Trace("strings-regexp-nf") << "Term " << atom << " is normalized to " << x << " IN " << r << std::endl; - if (e == 0) - { - // remember that we have unfolded a membership for x - repUnfold.insert(x); - } if (changed) { Node tmp = Rewriter::rewrite(nm->mkNode(STRING_IN_REGEXP, x, r)); @@ -246,7 +241,11 @@ void RegExpSolver::check() } } - if (repUnfold.find(x) != repUnfold.end()) + if (e == 0) + { + // remember that we have unfolded a membership for x + repUnfold.insert(x); + } else if (repUnfold.find(x) != repUnfold.end()) { // do not unfold negative memberships of strings that have new // positive unfoldings. For example: |