projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 47f71a6) | patch
Fix handling of non-standard re.range terms (#6563)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 19 May 2021 00:59:09 +0000 (19:59 -0500)
committerGitHub <noreply@github.com>
Wed, 19 May 2021 00:59:09 +0000 (00:59 +0000)
commit9ee8b184d9e97ae241ff079803b82859ed014dfa
treec82137409293b477d606a111e0932158563ed9f9tree
parent47f71a6d94b600cf7c132569fa05ad1666edc408commit | diff
Fix handling of non-standard re.range terms (#6563)

Fixes #6561. That benchmark now gives an error:
(error "expecting a single constant string term in regexp range").

This PR also makes isConstRegExp do a non-recursive dag traversal.
src/theory/strings/regexp_entail.cpp diff | blob | history
src/theory/strings/regexp_entail.h diff | blob | history
src/theory/strings/sequences_rewriter.cpp diff | blob | history