projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a6c001e) | patch
Fix regular expression consume for nested star (#5518)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 23 Nov 2020 22:09:20 +0000 (16:09 -0600)
committerGitHub <noreply@github.com>
Mon, 23 Nov 2020 22:09:20 +0000 (16:09 -0600)
commit07c7b873c5c2ee81cb2672428ca1de0d75bb1ae8
treec89e29818dc79cd6cc37360f9ce71257520f5406tree
parenta6c001e078767a2de6f36a2fa1333b98e39a6ec8commit | diff
Fix regular expression consume for nested star (#5518)

The issue was caused by simple regular expression consume being too aggressive when a recursive call was made to the method. In particular, we were assuming that the body of the star must be unrolled to fully consume a string, when it can be skipped if we are not at top level.

Fixes #5510.
src/theory/strings/regexp_entail.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/strings/issue5510-re-consume.smt2 [new file with mode: 0644] blob