projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 93a3d6a) | patch
Fix re-elim length requirement for symbolic RE memberships (#6609)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 24 May 2021 16:15:12 +0000 (11:15 -0500)
committerGitHub <noreply@github.com>
Mon, 24 May 2021 16:15:12 +0000 (16:15 +0000)
commit1516e3b5d9436be86841a52002fc728fcd52dd34
tree169d18bb732c4128a6251f2977c0ced772e5c603tree
parent93a3d6a65db331008d590c4bb7fc0658ff1e46e0commit | diff
Fix re-elim length requirement for symbolic RE memberships (#6609)

Fixes #6604.

Previously, re-elim was solution unsound for cases where the LHS and a component of the RHS were both empty. This ensures a length requirement is given for the LHS to ensure proper containment.
src/theory/strings/regexp_elim.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/strings/issue6604-re-elim.smt2 [new file with mode: 0644] blob