max element of sequence possible bug (?)

[OrenGitHub]

Hi,
This stack overflow question revealed what seems to be a bug:

(declare-fun max ((Seq Int)) Int)
(assert (forall ((A (Seq Int))) (=> (> (seq.len A) 0) (<= 0 (max A)))))
(assert (forall ((A (Seq Int))) (=> (> (seq.len A) 0) (< (max A) (seq.len A)))))
(assert (forall ((A (Seq Int)) (i Int)) (=> (and (> (seq.len A) 0) (<= 0 i) (< i (seq.len A)))
                        (<= (seq.nth A i) (seq.nth A (max A))))))

 (assert (= (max (seq.++ (seq.unit 8) (seq.unit 3))) 0))
;(assert (= (max (seq.++ (seq.unit 8) (seq.unit 3))) 1))

(check-sat)
(get-model)

And I get a wrong sat answer:

sat
(model 
  (define-fun max ((x!0 (Seq Int))) Int
    (ite (= x!0 (seq.++ (seq.unit 7718) (seq.++ (seq.unit 15) (seq.unit 7719))))
      2
      0))
)

[NikolajBjorner]

now it simply will not produce a model