projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c7116b0) | patch
Fix cases of ITE within regular expressions (#6783)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 22 Jun 2021 03:50:29 +0000 (22:50 -0500)
committerGitHub <noreply@github.com>
Tue, 22 Jun 2021 03:50:29 +0000 (22:50 -0500)
commit90d19f7cdbaf41e389bdcbd099471f658a35ce98
treea3ad5e82ec7c1bf751a7432abe63fec300867f10tree
parentc7116b06892b5ff21fb04a3996880bfe48e44053commit | 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.")
src/theory/strings/regexp_entail.cpp diff | blob | history