projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a1624b7) | patch
`STRINGS_CTN_DECOMPOSE`: Avoid multiple conflicts (#6632)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 28 May 2021 03:28:20 +0000 (20:28 -0700)
committerGitHub <noreply@github.com>
Fri, 28 May 2021 03:28:20 +0000 (20:28 -0700)
commit972dcfafe5eeb10b7b45892d1291000e73746c76
tree114c1210c913a7d6dd4ece1bcca700d0f1ac1f53tree
parenta1624b7f5b7809329845f4a31e7b6a0e86ebc9d3commit | diff
`STRINGS_CTN_DECOMPOSE`: Avoid multiple conflicts (#6632)

Fixes #5508. `STRINGS_CTN_DECOMPOSE` could be triggered multiple times
by the same term, which resulted in an assertion failure. This commit
returns immediately after the first conflict to avoid the assertion
failure.
src/theory/strings/extf_solver.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/strings/issue5508-multiple-conflicts.smt2 [new file with mode: 0644] blob