; reqproof verify-lemma — Phase E orchestrator
(define-fun-rec FirstNegative_loop_0 ((items (Seq Int)) (i Int)) Int
  (ite (and (< i (seq.len items)) (>= (seq.nth items i) 0))
    (let ((i$1 (+ i 1))) (FirstNegative_loop_0 items i$1))
    i))
(define-fun FirstNegative ((items (Seq Int))) Int (let ((i 0)) (let ((i$1 1)) (let ((i$2 (ite (> (seq.len items) 0) i$1 i))) (FirstNegative_loop_0 items i$2)))))
(define-fun proof_scan_bounds ((items (Seq Int))) Bool (let ((result (FirstNegative items))) (and (<= 0 result) (<= result (seq.len items)))))
(declare-fun items () (Seq Int))
(assert (=> (and (forall ((items (Seq Int))) (let ((i 0)) (let ((i$1 1)) (let ((i$2 (ite (> (seq.len items) 0) i$1 i))) (and (<= 0 i$2) (<= i$2 (seq.len items))))))) (forall ((items (Seq Int)) (i Int)) (=> (and (and (<= 0 i) (<= i (seq.len items))) (and (< i (seq.len items)) (>= (seq.nth items i) 0))) (let ((i$1 (+ i 1))) (and (<= 0 i$1) (<= i$1 (seq.len items))))))) (forall ((items (Seq Int)) (i Int)) (=> (and (<= 0 i) (<= i (seq.len items))) (and (<= 0 (FirstNegative_loop_0 items i)) (<= (FirstNegative_loop_0 items i) (seq.len items)))))))
(assert (and (<= 0 (seq.len items)) (<= (seq.len items) 32)))
(assert (not (and (forall ((items (Seq Int))) (let ((i 0)) (let ((i$1 1)) (let ((i$2 (ite (> (seq.len items) 0) i$1 i))) (and (<= 0 i$2) (<= i$2 (seq.len items))))))) (forall ((items (Seq Int)) (i Int)) (=> (and (and (<= 0 i) (<= i (seq.len items))) (and (< i (seq.len items)) (>= (seq.nth items i) 0))) (let ((i$1 (+ i 1))) (and (<= 0 i$1) (<= i$1 (seq.len items)))))) (proof_scan_bounds items))))
(check-sat)
(get-model)