diff options
Diffstat (limited to 'src/theory/strings/regexp_solver.cpp')
| -rw-r--r-- | src/theory/strings/regexp_solver.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp index 4187a667e..f2d87e6da 100644 --- a/src/theory/strings/regexp_solver.cpp +++ b/src/theory/strings/regexp_solver.cpp @@ -194,7 +194,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems) addedLemma = true; break; } - } else if (polarity && tmp != nm->mkNode(STRING_IN_REGEXP, nx, r)) { + } else if (polarity && nx.getKind() == STRING_CONCAT && tmp != nm->mkNode(STRING_IN_REGEXP, nx, r)) { std::vector<Node> exp_n; exp_n.push_back(assertion); Node conc = tmp; |