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 /src/api/python/cvc5.pxi | |
| 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.")
Diffstat (limited to 'src/api/python/cvc5.pxi')
0 files changed, 0 insertions, 0 deletions