diff options
Diffstat (limited to 'src/theory/strings/regexp_solver.cpp')
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 16 |
1 files changed, 1 insertions, 15 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 2d4404c10..7737a90f7 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -96,7 +96,6 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) bool addedLemma = false; bool changed = false; std::vector<Node> processed; - std::vector<Node> cprocessed; Trace("regexp-process") << "Checking Memberships ... " << std::endl; for (const std::pair<const Node, std::vector<Node> >& mr : mems) @@ -287,14 +286,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) polarity ? InferenceId::STRINGS_RE_UNFOLD_POS : InferenceId::STRINGS_RE_UNFOLD_NEG; d_im.sendInference(iexp, noExplain, conc, inf); addedLemma = true; - if (changed) - { - cprocessed.push_back(assertion); - } - else - { - processed.push_back(assertion); - } + processed.push_back(assertion); if (e == 0) { // Remember that we have unfolded a membership for x @@ -326,12 +318,6 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) << "...add " << processed[i] << " to u-cache." << std::endl; d_regexp_ucached.insert(processed[i]); } - for (unsigned i = 0; i < cprocessed.size(); i++) - { - Trace("strings-regexp") - << "...add " << cprocessed[i] << " to c-cache." << std::endl; - d_regexp_ccached.insert(cprocessed[i]); - } } } } |