projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 53feec2) | patch
Fix type check of `seq.nth` (#8093)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 11 Feb 2022 00:21:06 +0000 (16:21 -0800)
committerGitHub <noreply@github.com>
Fri, 11 Feb 2022 00:21:06 +0000 (16:21 -0800)
commit50d93bfc5bcd160059522e22310934ea4ecb2c57
treed2b1a09420fe59ea5758dd3e4778ebc46e189492tree
parent53feec296fd26985c4a6d5ead19ff9ef53c5ce7fcommit | diff
Fix type check of `seq.nth` (#8093)

The code for type checking `seq.nth` was trying to retrieve the sequence
element type before ensuring that the type of the first argument was a
sequence, which lead to assertion failures. This commit reorders the
checks to avoid this issue.
src/theory/strings/theory_strings_type_rules.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/seq/seq-nth-type-check.smt2 [new file with mode: 0644] blob