summaryrefslogtreecommitdiff
path: root/src/theory/strings
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-06-30 18:08:54 -0500
committerGitHub <noreply@github.com>2020-06-30 18:08:54 -0500
commitffed5a43764641d4808aa77bb0e393623fd4442d (patch)
treeea8af32d4c457dc153a52bd29f76994f09c84149 /src/theory/strings
parentd00ee06575318e4fa901f3367e76883bf8692cd9 (diff)
Fix normal form for re.comp (#4676)
Fixes #4674.
Diffstat (limited to 'src/theory/strings')
-rw-r--r--src/theory/strings/regexp_solver.cpp1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 627258a4c..53c6c9acc 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -672,6 +672,7 @@ Node RegExpSolver::getNormalSymRegExp(Node r, std::vector<Node>& nf_exp)
case REGEXP_UNION:
case REGEXP_INTER:
case REGEXP_STAR:
+ case REGEXP_COMPLEMENT:
{
std::vector<Node> vec_nodes;
for (const Node& cr : r)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback