diff options
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index b13b64f98..0716bae1a 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -194,6 +194,14 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) addedLemma = true; break; } + } else if (polarity) { + std::vector<Node> exp_n; + exp_n.push_back(assertion); + Node conc = tmp; + d_im.sendInference(nfexp, exp_n, conc, "REGEXP NF simp"); + addedLemma = true; + d_parent.getExtTheory()->markReduced(assertion); + continue; } } if (e == 1 && repUnfold.find(rep) != repUnfold.end()) |