projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cb68fa0) | patch
Fix non-termination issues in simpleRegExpConsume (#4667)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 28 Jun 2020 13:34:44 +0000 (08:34 -0500)
committerGitHub <noreply@github.com>
Sun, 28 Jun 2020 13:34:44 +0000 (08:34 -0500)
commit46591b1c92fc9ecd4a0997242030a1a48166301b
tree83ef7b9262e31957bebd685e3be0c943f8c01d64tree
parentcb68fa0f7b096bf086a7c7189e40805253ef1acfcommit | diff
Fix non-termination issues in simpleRegExpConsume (#4667)

There were two issues related to RE in bodies of re.* that accepted the empty string that led to non-termination in the rewriter for regular expressions.

This also improves trace messages for simpleRegExpConsume.

Fixes #4662.
src/theory/strings/regexp_entail.cpp diff | blob | history
src/theory/strings/sequences_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/strings/issue4662-consume-nterm.smt2 [new file with mode: 0644] blob