(proof) Assertion error at smt_conflict_resolution.cpp:1141

[rainoftime]

Hi, for the following formula,
z3 4db41c0

(set-option :proof true)
(declare-fun v0 () Bool)
(declare-fun i1 () Int)
(declare-fun arr-5454958627128445793_5454958627128445793-0 () (Array Bool Bool))
(declare-fun v6 () Bool)
(declare-fun i6 () Int)
(declare-fun arr-5454958627128445793_2742809287566591043-0 () (Array Bool (Array Bool Bool)))
(declare-fun arr--7827409692447274155_1253340784302488146-0 () (Array (Array (Array Bool Bool) Bool) (Array Int (Array (Array Bool Bool) Bool))))
(declare-fun arr-2742809287566591043_-1746939430831302062-0 () (Array (Array Bool Bool) (Array (Array (Array Bool Bool) Bool) (Array Int (Array (Array Bool Bool) Bool)))))
(declare-fun v60 () Bool)
(declare-fun arr-8505173358366493644_5454958627128445793-2 () (Array (Array (Array Bool Bool) (Array (Array (Array Bool Bool) Bool) (Array Int (Array (Array Bool Bool) Bool)))) Bool))
(assert (and v60 (= v60 (and (= 0 i1) (= i6 (abs i1))))))
(assert (! (or v6 (= arr-8505173358366493644_5454958627128445793-2 (store arr-8505173358366493644_5454958627128445793-2 (store (store arr-2742809287566591043_-1746939430831302062-0 arr-5454958627128445793_5454958627128445793-0 (select arr-2742809287566591043_-1746939430831302062-0 (store arr-5454958627128445793_5454958627128445793-0 v0 true))) (select arr-5454958627128445793_2742809287566591043-0 (= i6 (abs i1))) arr--7827409692447274155_1253340784302488146-0) true))) :named IP_190))
(check-sat-assuming (IP_190))

z3 delta.out.smt2 
ASSERTION VIOLATION
File: ../src/smt/smt_conflict_resolution.cpp
Line: 1141
UNEXPECTED CODE WAS REACHED.
Z3 4.8.10.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new