projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e95e704) | patch
Fix spurious antecedant for symbolic regular expressions (#6284)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 5 Apr 2021 20:52:20 +0000 (15:52 -0500)
committerGitHub <noreply@github.com>
Mon, 5 Apr 2021 20:52:20 +0000 (20:52 +0000)
commit3c98bb2e9abdb2542ac794f161d0f199c1cfaeaf
tree12de562c61aae8ad066fcd33444ab4ee639d822btree
parente95e704f362690377d851fe80bbc778877bbfc69commit | diff
Fix spurious antecedant for symbolic regular expressions (#6284)

Fixes #6271.

This was triggered by recent fixes, this fixes solution soundness issues with symbolic regular expressions due to spuriously included antecedants, which made lemmas SAT-context dependent while being cached as user-context dependent.
src/theory/strings/regexp_solver.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/strings/issue6271-2-rnf.smt2 [new file with mode: 0644] blob
test/regress/regress1/strings/issue6271-rnf.smt2 [new file with mode: 0644] blob