projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ef48e42) | patch
Fix non-termination in the strings rewriter (#8438)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 31 Mar 2022 02:08:18 +0000 (21:08 -0500)
committerGitHub <noreply@github.com>
Thu, 31 Mar 2022 02:08:18 +0000 (02:08 +0000)
commit600685caae205a9abe6bd7d821f5b2716f6f7520
tree4e417bd9fbaf170136d6b12c0854ab7a08932276tree
parentef48e42744b158a077abdf1299ce9e53da87379fcommit | diff
Fix non-termination in the strings rewriter (#8438)

Fixes #8434.

This makes our component containment utility less aggressive. This impacts (seldom used) rewrites for indexof and replace only.
src/theory/rewriter.cpp diff | blob | history
src/theory/strings/strings_entail.cpp diff | blob | history
src/theory/strings/strings_entail.h diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress1/strings/issue8434-nterm-str-rw.smt2 [new file with mode: 0644] blob