projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d036ca9) | patch
[Seq] Check types for split on indices (#8066)
authorAndres Noetzli <andres.noetzli@gmail.com>
Sun, 6 Feb 2022 08:16:48 +0000 (00:16 -0800)
committerGitHub <noreply@github.com>
Sun, 6 Feb 2022 08:16:48 +0000 (08:16 +0000)
commita95f8979d8bd15f11427aaf7f69663959756dd42
treedd8b3960c75a67a4de41ec72a9492984f3544944tree
parentd036ca9091767e31b41fc76afabd0cc6c451f153commit | diff
[Seq] Check types for split on indices (#8066)

We applied `STRINGS_ARRAY_EQ_SPLIT` to pairs of `seq.nth` terms of
different types. This lead to assertion (in debug) and performance
problems (in production). The commit adds a type check.
src/theory/strings/array_core_solver.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/seq/mixed-types-seq-nth.smt2 [new file with mode: 0644] blob