Assertion violation at smt/smt_model_finder.cpp:2387 (smt.clause_proof )

[rainoftime]

Hi, for the following formula,
assert.txt

When executing the command

z3 fname.smt2 --timeout 10000

z3 (commit dde0c51) throws an assertion violation

sat
sat
sat
(error "line 119 column 7: canceled")
ASSERTION VIOLATION
File: ../src/smt/smt_model_finder.cpp
Line: 2387
m_ftodo.empty()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

Reduced

(set-logic UFBV)
(declare-fun _substvar_107_ () (_ BitVec 37))
(declare-fun _substvar_417_ () (_ BitVec 37))
(declare-fun _substvar_418_ () (_ BitVec 37))
(declare-fun _substvar_575_ () (_ BitVec 37))
(declare-fun _substvar_644_ () (_ BitVec 29))
(declare-fun _substvar_649_ () (_ BitVec 37))
(declare-fun _substvar_652_ () (_ BitVec 29))
(declare-fun _substvar_653_ () Bool)
(declare-fun _substvar_674_ () Bool)
(declare-fun _substvar_415_ () Bool)
(declare-fun _substvar_529_ () Bool)
(declare-fun _substvar_618_ () Bool)
(set-option :model_validate true)
(set-option :unsat_core true)
(set-option :smt.clause_proof true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(check-sat)
(declare-const v11 Bool)
(declare-const bv_29-0 (_ BitVec 29))
(check-sat)
(check-sat)
(push 1)
(declare-const v15 Bool)
(declare-const bv_15-0 (_ BitVec 15))
(assert (! (distinct true true true true (or true true _substvar_415_ (xor v9 v15 (= (_ bv0 29) (_ bv0 29) (_ bv0 29)) true true true _substvar_529_ _substvar_618_ v8 v3) true)) :named IP_25))
(declare-sort S1 0)
(pop 1)
(assert (! true :named IP_50))
(assert (! false :named IP_61))
(assert (! (or (forall ((q56 (_ BitVec 37)) (q57 (_ BitVec 37)) (q58 (_ BitVec 37)) (q59 (_ BitVec 37))) (not (distinct (_ bv0 37) q59 _substvar_575_))) (exists ((q56 (_ BitVec 37)) (q57 (_ BitVec 37)) (q58 (_ BitVec 37)) (q59 (_ BitVec 37))) (not (distinct (_ bv0 37) (bvudiv (_ bv0 37) _substvar_107_) (bvudiv (_ bv0 37) (bvudiv (_ bv0 37) _substvar_418_)))))) :named IP_64))
(assert (! (forall ((q71 (_ BitVec 29))) (= (_ bv0 29) (_ bv0 29) q71)) :named IP_74))
(push 1)
(check-sat)