Segmentation fault

[junzew]

Hi, for the following program

(set-logic ALL)
(declare-fun skoT () Real)
(declare-fun skoB () Real)
(declare-fun skoA () Real)
(declare-fun skoS () Real)
(assert (let ((?v_3 (* skoA skoA))(?v_0 (<= 0 skoT))) (let ((?v_1 (not ?v_0))(?v_2 (* skoB (- 1)))) (or (>= (- skoT (+ skoT (abs 3))) ?v_3) (and ?v_1 (and (or ?v_0 (< skoT ?v_2)) (and (or (<= skoB skoT) (>= skoT 0)) (and (=> (not (> (abs 1) skoT)) ?v_0) (or (or ?v_1 (not (> skoT 1))) (or (distinct (* skoT (* skoT (+ (* (+ skoA (* skoA (- 1))) (- skoB ?v_2)) (* skoT (+ skoT (abs 1)))))) (+ (- skoB (- skoB ?v_3)) (* skoS (- skoS (abs 1))))) (or (> 0 skoS) (and (not (> skoA 0)) (or (not (> 2 skoB)) (not (< skoB skoA)))))))))))))))
(check-sat)
(exit)

z3 crashes and gives a segmentation fault.
but cvc4 outputs sat.
Z3 version 4.8.9