Z3 crash with Seq Int

[OrenGitHub]

Hi,
The following smt file crashes:

;;;;;;;;;;;;;;;;;;;;;
;                   ;
; This is our state ;
;                   ;
;;;;;;;;;;;;;;;;;;;;;
(declare-datatypes ((State 0))
    (((rec
        (myArray (Seq Int))
		(used    (Seq Bool))
        (index   Int)
		(out     Bool)
		(res     Bool))))
)

;;;;;;;;;;;;;;;;;;;;;;;;
;                      ;
; some arbitrary state ;
;                      ;
;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const sigma State)

;;;;;;;;;;;;;;;;
;              ;
; (n-1) values ;
;              ;
;;;;;;;;;;;;;;;;
(declare-const n1 Int)
(assert (= n1 (seq.len (myArray sigma))))

;;;;;;;;;;;;;;;;
;              ;
; (n-1) values ;
;              ;
;;;;;;;;;;;;;;;;
(declare-const s1 (Seq Int))
(assert (= s1 (myArray sigma)))

;;;;;;;;;;;;;;;;
;              ;
; (n-1) values ;
;              ;
;;;;;;;;;;;;;;;;
(declare-const m1 Int)

;;;;;;;;;;;;;;;;
;              ;
; (n-1) values ;
;              ;
;;;;;;;;;;;;;;;;
(assert (<= 0 m1))

;;;;;;;;;;;;;;;;
;              ;
; (n-1) values ;
;              ;
;;;;;;;;;;;;;;;;
(assert (< m1 n1))

;;;;;;;;;;;;;;;;
;              ;
; (n-1) values ;
;              ;
;;;;;;;;;;;;;;;;
(assert (=> (seq.contains s1 (seq.unit (- n1 1))) (= (seq.nth s1 m1) (- n1 1))))

;;;;;;;;;;;;;;;;
;              ;
; (n-1) values ;
;              ;
;;;;;;;;;;;;;;;;
(declare-const w1 (Seq Int))

;;;;;;;;;;;;;;;;
;              ;
; (n-1) values ;
;              ;
;;;;;;;;;;;;;;;;
(declare-const w1_tag (Seq Int))

;;;;;;;;;;;;;;;;
;              ;
; (n-1) values ;
;              ;
;;;;;;;;;;;;;;;;
(assert (=> (seq.contains s1 (seq.unit (- n1 1))) (= (seq.++ (seq.++ w1 (seq.at s1 m1)) w1_tag) (myArray sigma))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                          ;
; init predicate on states ;
;                          ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(define-fun init ((in State)) Bool
	(and
		(seq.in.re (used in) (re.* (seq.to.re (seq.unit false))))
		(not (out in))
		(= (index in) 0))
)

(assert (< 0 (seq.len (myArray sigma))))
(assert (< 0 (seq.len (used    sigma))))

;;;;;;;;;;;
;         ;
; f_sigma ;
;         ;
;;;;;;;;;;;
(declare-const f_sigma State)
(assert (= f_sigma
	(let (
		(s (myArray sigma))
		(i (index   sigma))
		(u (used    sigma))
		(o (out     sigma))
		(r (res     sigma))
		(n (seq.len (myArray sigma)))
		(s0 (seq.nth (myArray sigma) 0))
		(seq_n_minus_1 (seq.unit (- (seq.len (myArray sigma)) 1)))
		(seq_74 (seq.unit 74))
		(seq_false (seq.unit false))
		(s_without_0 (seq.extract (myArray sigma) 1 (- (seq.len (myArray sigma)) 1)))
		(u_without_n (seq.extract (used    sigma) 0 (- (seq.len (used    sigma)) 1))))
	(ite
		(>= s0 n)
		(rec seq_74 seq_false 0 o r)
		(ite
			(seq.contains w1 seq_n_minus_1)
			(rec seq_74 seq_false 1 o r)
			(rec w1 u_without_n   i o r))))))


(assert
(and
	     (init   sigma)
	(not (init f_sigma))))

;;;;;;;;;;;;;;;;;;;;;;;;;
;                       ;
; check sat + get model ;
;                       ;
;;;;;;;;;;;;;;;;;;;;;;;;;
(check-sat)
(get-model)

Unfortunately, I couldn't make it any smaller than this.
I get the following error:

ASSERTION VIOLATION
File: ../src/smt/theory_seq.cpp
Line: 5546
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB