diff options
Diffstat (limited to 'src/theory/strings/regexp_solver.cpp')
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 7737a90f7..0db536d1b 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -284,16 +284,21 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) } InferenceId inf = polarity ? InferenceId::STRINGS_RE_UNFOLD_POS : InferenceId::STRINGS_RE_UNFOLD_NEG; - d_im.sendInference(iexp, noExplain, conc, inf); - addedLemma = true; - processed.push_back(assertion); - if (e == 0) + // in very rare cases, we may find out that the unfolding lemma + // for a membership is equivalent to true, in spite of the RE + // not being rewritten to true. + if (d_im.sendInference(iexp, noExplain, conc, inf)) { - // Remember that we have unfolded a membership for x - // notice that we only do this here, after we have definitely - // added a lemma. - repUnfold.insert(rep); + addedLemma = true; + if (e == 0) + { + // Remember that we have unfolded a membership for x + // notice that we only do this here, after we have definitely + // added a lemma. + repUnfold.insert(rep); + } } + processed.push_back(assertion); } else { |