diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-09 23:34:57 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-09 23:34:57 -0800 |
commit | 80158863a9cccff67e7e6aa58ccc9a5c63174439 (patch) | |
tree | ec558a2f5b2a75a7d1fb3a65e7adec3b2964f6c3 | |
parent | dae98f0a3338ad8754bcd69c4ac26ca82d786af7 (diff) |
test
-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; |