projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8ac648b) | patch
Fix indexof_re reduction (#8065)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 7 Feb 2022 18:17:13 +0000 (12:17 -0600)
committerGitHub <noreply@github.com>
Mon, 7 Feb 2022 18:17:13 +0000 (18:17 +0000)
commitf4b167eb29e2716e996450d844a8bd4de626d7f6
tree3aecb3b0ca98cf08e2568350b041c56ac4a4405etree
parent8ac648bebbbb0621d83689f66f7180ca33cf6534commit | diff
Fix indexof_re reduction (#8065)

Fixes https://github.com/cvc5/cvc5/issues/6654.

Note that this regression now answers unknown with `--ext-rewrite-quant`; the regression without this option is added.
src/theory/strings/theory_strings_preprocess.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/strings/issue6654-indexof_re_red.smt2 [new file with mode: 0644] blob