diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-19 09:36:53 -0400 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-07-19 09:36:53 -0400 |
| commit | 9fa66413709fbdb1a02f8986d0c332934523b110 (patch) | |
| tree | 39b67dd05ba658c1f8619d3b5156f453f895ea64 /src/theory/strings/regexp_solver.cpp | |
| parent | d5ed6a659eaa801fbbd82efc31f03d575351b6ec (diff) | |
Fix case of unfolding negative membership in reg exp concatenation (#3101)
Diffstat (limited to 'src/theory/strings/regexp_solver.cpp')
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 5079806ac..65d616c3c 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -281,7 +281,6 @@ void RegExpSolver::check() std::vector<Node> exp_n; exp_n.push_back(assertion); Node conc = nvec.size() == 1 ? nvec[0] : nm->mkNode(AND, nvec); - conc = Rewriter::rewrite(conc); d_im.sendInference(rnfexp, exp_n, conc, "REGEXP_Unfold"); addedLemma = true; if (changed) |