seq.indexOf with a non-0 start

[LeventErkok]

This is quite similar to #4076, except we start searching not at the beginning but in the middle somewhere:

(set-option :produce-models true)
(set-logic ALL)
(define-fun s0 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3)))
(define-fun s1 () (Seq Int) (seq.unit 2))
(declare-fun s2 () Int)
(assert (= s2 (seq.indexof s0 s1 1)))
(check-sat)
(get-value (s2))

The value of s2 must be 1, but we're getting:

$ z3 a.smt2
sat
((s2 0))