Segmentation fault with sequence benchmark

[LeventErkok]

The following benchmark has two calls to check-sat. If you comment the first one out, z3 answers the query. (Though I did not check the correctness of the response.)

Unfortunately, if you keep both calls to check-sat as given below, then z3 gives a segmentation fault and crashes on Mac OSX. This is with a z3 that was built out of master two days ago.

I can try to minimize the output if it would help. Let me know.

(set-logic ALL)
(define-fun s2 () Int 4)
(define-fun s4 () Int 0)
(define-fun s6 () (Seq Bool) (as seq.empty (Seq Bool)))
(define-fun s8 () Int 2)
(define-fun s11 () Int 1)
(declare-fun s0 () (Seq Int))
(define-fun s1 () Int (seq.len s0))
(define-fun s3 () Bool (= s1 s2))
(define-fun s5 () Bool (= s1 s4))
(define-fun s7 () Int (seq.nth s0 s4))
(define-fun s9 () Bool (< s7 s8))
(define-fun s10 () (Seq Bool) (seq.unit s9))
(define-fun s12 () Int (- s1 s11))
(define-fun s13 () (Seq Int) (seq.extract s0 s11 s12))
(define-fun s14 () Int (seq.len s13))
(define-fun s15 () Bool (= s4 s14))
(define-fun s16 () Int (seq.nth s13 s4))
(define-fun s17 () Bool (< s16 s8))
(define-fun s18 () (Seq Bool) (seq.unit s17))
(define-fun s19 () Int (- s14 s11))
(define-fun s20 () (Seq Int) (seq.extract s13 s11 s19))
(define-fun s21 () Int (seq.len s20))
(define-fun s22 () Bool (= s4 s21))
(define-fun s23 () Int (seq.nth s20 s4))
(define-fun s24 () Bool (< s23 s8))
(define-fun s25 () (Seq Bool) (seq.unit s24))
(define-fun s26 () Int (- s21 s11))
(define-fun s27 () (Seq Int) (seq.extract s20 s11 s26))
(define-fun s28 () Int (seq.len s27))
(define-fun s29 () Bool (= s4 s28))
(define-fun s30 () Int (seq.nth s27 s4))
(define-fun s31 () Bool (< s30 s8))
(define-fun s32 () (Seq Bool) (seq.unit s31))
(define-fun s33 () (Seq Bool) (ite s29 s6 s32))
(define-fun s34 () (Seq Bool) (seq.++ s25 s33))
(define-fun s35 () (Seq Bool) (ite s22 s6 s34))
(define-fun s36 () (Seq Bool) (seq.++ s18 s35))
(define-fun s37 () (Seq Bool) (ite s15 s6 s36))
(define-fun s38 () (Seq Bool) (seq.++ s10 s37))
(define-fun s39 () (Seq Bool) (ite s5 s6 s38))
(define-fun s40 () Int (seq.len s39))
(define-fun s41 () Bool (= s4 s40))
(define-fun s42 () Bool (seq.nth s39 s4))
(define-fun s43 () Int (- s40 s11))
(define-fun s44 () (Seq Bool) (seq.extract s39 s11 s43))
(define-fun s45 () Int (seq.len s44))
(define-fun s46 () Bool (= s4 s45))
(define-fun s47 () Bool (seq.nth s44 s4))
(define-fun s48 () Int (- s45 s11))
(define-fun s49 () (Seq Bool) (seq.extract s44 s11 s48))
(define-fun s50 () Int (seq.len s49))
(define-fun s51 () Bool (= s4 s50))
(define-fun s52 () Bool (seq.nth s49 s4))
(define-fun s53 () Int (- s50 s11))
(define-fun s54 () (Seq Bool) (seq.extract s49 s11 s53))
(define-fun s55 () Int (seq.len s54))
(define-fun s56 () Bool (= s4 s55))
(define-fun s57 () Bool (seq.nth s54 s4))
(define-fun s58 () Bool (or s56 s57))
(define-fun s59 () Bool (and s52 s58))
(define-fun s60 () Bool (or s51 s59))
(define-fun s61 () Bool (and s47 s60))
(define-fun s62 () Bool (or s46 s61))
(define-fun s63 () Bool (and s42 s62))
(define-fun s64 () Bool (or s41 s63))
(define-fun s65 () Bool (>= s7 s4))
(define-fun s66 () (Seq Bool) (seq.unit s65))
(define-fun s67 () Bool (>= s16 s4))
(define-fun s68 () (Seq Bool) (seq.unit s67))
(define-fun s69 () Bool (>= s23 s4))
(define-fun s70 () (Seq Bool) (seq.unit s69))
(define-fun s71 () Bool (>= s30 s4))
(define-fun s72 () (Seq Bool) (seq.unit s71))
(define-fun s73 () (Seq Bool) (ite s29 s6 s72))
(define-fun s74 () (Seq Bool) (seq.++ s70 s73))
(define-fun s75 () (Seq Bool) (ite s22 s6 s74))
(define-fun s76 () (Seq Bool) (seq.++ s68 s75))
(define-fun s77 () (Seq Bool) (ite s15 s6 s76))
(define-fun s78 () (Seq Bool) (seq.++ s66 s77))
(define-fun s79 () (Seq Bool) (ite s5 s6 s78))
(define-fun s80 () Int (seq.len s79))
(define-fun s81 () Bool (= s4 s80))
(define-fun s82 () Bool (seq.nth s79 s4))
(define-fun s83 () Int (- s80 s11))
(define-fun s84 () (Seq Bool) (seq.extract s79 s11 s83))
(define-fun s85 () Int (seq.len s84))
(define-fun s86 () Bool (= s4 s85))
(define-fun s87 () Bool (seq.nth s84 s4))
(define-fun s88 () Int (- s85 s11))
(define-fun s89 () (Seq Bool) (seq.extract s84 s11 s88))
(define-fun s90 () Int (seq.len s89))
(define-fun s91 () Bool (= s4 s90))
(define-fun s92 () Bool (seq.nth s89 s4))
(define-fun s93 () Int (- s90 s11))
(define-fun s94 () (Seq Bool) (seq.extract s89 s11 s93))
(define-fun s95 () Int (seq.len s94))
(define-fun s96 () Bool (= s4 s95))
(define-fun s97 () Bool (seq.nth s94 s4))
(define-fun s98 () Bool (or s96 s97))
(define-fun s99 () Bool (and s92 s98))
(define-fun s100 () Bool (or s91 s99))
(define-fun s101 () Bool (and s87 s100))
(define-fun s102 () Bool (or s86 s101))
(define-fun s103 () Bool (and s82 s102))
(define-fun s104 () Bool (or s81 s103))
(assert s3)
(assert s64)
(assert s104)
(check-sat)       ; COMMENT THIS OUT AND SEG FAULT GOES AWAY
(define-fun s105 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 0) (seq.unit 0) (seq.unit 1)))
(define-fun s106 () Bool (distinct s0 s105))
(assert s106)
(check-sat)
(get-value (s0))

[NikolajBjorner]

this one is fixed now