[Seq] Fix rewrite of `(seq.nth s n)` for large `n` (#8083)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 9 Feb 2022 04:58:23 +0000 (20:58 -0800)
committerGitHub <noreply@github.com>
Wed, 9 Feb 2022 04:58:23 +0000 (22:58 -0600)
commitb07543b20ab2e263035b75aca0b92636f5a9cdcb
tree261ccf5ae2f5420c9dabf04e1d906750a2dd3e22
parentc93eccb4706804ffc139548f9d2f2145fda820a9
[Seq] Fix rewrite of `(seq.nth s n)` for large `n` (#8083)

When rewriting (seq.nth s n) where both terms are constants, cvc5 was
blindly converting the n to a uint32_t, which caused issues when n
was greater than the largest value that can be represented by a 32-bit
integer. This commit introduces a corresponding check and does not
perform the rewrite for large n.
src/theory/strings/sequences_rewriter.cpp
test/unit/theory/sequences_rewriter_white.cpp