ASSERTION VIOLATION File: ../src/util/parray.h Line: 333 with `proof=true`

[wingsyuyi-satori]

Hello, I encountered an assertion violation when running Z3 debug build on the following input with proof=true.
The original test case was syntactically correct. The input provided below is a result of minimization using ddsmt. Although this reduced version appears to contain syntax errors (e.g., missing bodies in let expressions), it still triggers the exact same assertion violation as the original valid input.
Input :

(set-option :produce-unsat-cores true)
(declare-const s (_ BitVec 8))
(assert (or (and (= s (let ((s_int (_ bv0 8))))) (= s (_ bv1 8))) (and (= s (_ bv1 8)) (= s (let ((ubv_to_int (_ bv0 8))))))))
(assert (= (_ bv0 8) (ite false (_ bv0 8) ((_ int_to_bv 8) (div 0 (ubv_to_int (_ bv0 8)))))))
(check-sat)

Command : z3 test.smt2 proof=true
Output :

ASSERTION VIOLATION
File: ../src/util/parray.h
Line: 333
i < size(r)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB, Invoke (L)LDB

Commit : ec42464