projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f61ad69) | patch
Add lemma for the range of values of str.indexof (#3054)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 14 Jun 2019 01:39:10 +0000 (18:39 -0700)
committerGitHub <noreply@github.com>
Fri, 14 Jun 2019 01:39:10 +0000 (18:39 -0700)
commit2d478849d704f44f2a1f584dbc98d3731ca4e6ee
tree69b4559ecf894a939c6b333f76eb2d4df340a120tree
parentf61ad6919fc80cbc19fde9c295beb5082a6e0d79commit | diff
Add lemma for the range of values of str.indexof (#3054)

This commit adds a lemma that the value of `str.indexof(x, y, n)` must
be between -1 and `str.len(x)`.
src/theory/strings/theory_strings.cpp diff | blob | history