diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-21 22:50:29 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-21 22:50:29 -0500 |
commit | 90d19f7cdbaf41e389bdcbd099471f658a35ce98 (patch) | |
tree | a3ad5e82ec7c1bf751a7432abe63fec300867f10 | |
parent | c7116b06892b5ff21fb04a3996880bfe48e44053 (diff) |
Fix cases of ITE within regular expressions (#6783)
Fixes #6776.
Our computation of when a regular expression was constant did not account for when ITE was embedded in an RE, leading to an unsound rewrite.
That benchmark now gives:
(error "Regular expression variables are not supported.")
-rw-r--r-- | src/theory/strings/regexp_entail.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index 3d4a2d143..be1646403 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -364,6 +364,10 @@ bool RegExpEntail::isConstRegExp(TNode t) } } } + else if (ck == ITE) + { + return false; + } else if (cur.isVar()) { return false; |