Sequences, soundness

[LeventErkok]

This seems to be a recent breakage. z3 says unsat. It should actually be sat.

[I was originally confused by my Travis CI output and thought it was a Mac only failure. But that's not true. The failure seems to be platform independent; which is a good thing I suppose!]

(set-option :produce-models true)
(set-option :pp.max_depth      4294967295)
(set-option :pp.min_alias_size 4294967295)
(set-logic ALL)
(define-fun s14 () Int 1)
(define-fun s26 () Int 0)
(define-fun s12 () (Seq Int) (as seq.empty (Seq Int)))
(declare-fun s0 () Int) ; tracks user variable "a"
(declare-fun s1 () Int) ; tracks user variable "b"
(declare-fun s2 () Int) ; tracks user variable "c"
(declare-fun s23 () Int) ; tracks user variable "__internal_sbv_s23"
(declare-fun s34 () Int) ; tracks user variable "__internal_sbv_s34"
(declare-fun s41 () Int) ; tracks user variable "__internal_sbv_s41"
(declare-fun s55 () Int) ; tracks user variable "__internal_sbv_s55"
(declare-fun s69 () Int) ; tracks user variable "__internal_sbv_s69"
(declare-fun s93 () Int) ; tracks user variable "__internal_sbv_s93"
(declare-fun s100 () Int) ; tracks user variable "__internal_sbv_s100"
(declare-fun s114 () Int) ; tracks user variable "__internal_sbv_s114"
(declare-fun s128 () Int) ; tracks user variable "__internal_sbv_s128"
(define-fun s3 () Bool (<= s0 s1))
(define-fun s4 () Bool (<= s1 s2))
(define-fun s5 () Bool (and s3 s4))
(define-fun s6 () Bool (not s5))
(define-fun s7 () (Seq Int) (seq.unit s0))
(define-fun s8 () (Seq Int) (seq.unit s1))
(define-fun s9 () (Seq Int) (seq.unit s2))
(define-fun s10 () (Seq Int) (seq.++ s8 s9))
(define-fun s11 () (Seq Int) (seq.++ s7 s10))
(define-fun s13 () Bool (= s11 s12))
(define-fun s15 () Int (seq.len s11))
(define-fun s16 () Int (- s15 s14))
(define-fun s17 () (Seq Int) (seq.extract s11 s14 s16))
(define-fun s18 () Bool (= s12 s17))
(define-fun s19 () Int (seq.len s17))
(define-fun s20 () Int (- s19 s14))
(define-fun s21 () (Seq Int) (seq.extract s17 s14 s20))
(define-fun s22 () Bool (= s12 s21))
(define-fun s24 () (Seq Int) (seq.unit s23))
(define-fun s25 () Int (seq.len s21))
(define-fun s27 () Bool (> s25 s26))
(define-fun s28 () Bool (not s27))
(define-fun s29 () (Seq Int) (seq.extract s21 s26 s14))
(define-fun s30 () Bool (= s24 s29))
(define-fun s31 () Bool (or s28 s30))
(define-fun s32 () (Seq Int) (ite s22 s12 s24))
(define-fun s33 () Bool (= s12 s32))
(define-fun s35 () (Seq Int) (seq.unit s34))
(define-fun s36 () Bool (> s19 s26))
(define-fun s37 () Bool (not s36))
(define-fun s38 () (Seq Int) (seq.extract s17 s26 s14))
(define-fun s39 () Bool (= s35 s38))
(define-fun s40 () Bool (or s37 s39))
(define-fun s42 () (Seq Int) (seq.unit s41))
(define-fun s43 () Int (seq.len s32))
(define-fun s44 () Bool (> s43 s26))
(define-fun s45 () Bool (not s44))
(define-fun s46 () (Seq Int) (seq.extract s32 s26 s14))
(define-fun s47 () Bool (= s42 s46))
(define-fun s48 () Bool (or s45 s47))
(define-fun s49 () Bool (< s34 s41))
(define-fun s50 () Int (- s43 s14))
(define-fun s51 () (Seq Int) (seq.extract s32 s14 s50))
(define-fun s52 () (Seq Int) (seq.++ s42 s51))
(define-fun s53 () (Seq Int) (seq.++ s35 s52))
(define-fun s54 () Bool (= s12 s51))
(define-fun s56 () (Seq Int) (seq.unit s55))
(define-fun s57 () Int (seq.len s51))
(define-fun s58 () Bool (> s57 s26))
(define-fun s59 () Bool (not s58))
(define-fun s60 () (Seq Int) (seq.extract s51 s26 s14))
(define-fun s61 () Bool (= s56 s60))
(define-fun s62 () Bool (or s59 s61))
(define-fun s63 () Bool (< s34 s55))
(define-fun s64 () Int (- s57 s14))
(define-fun s65 () (Seq Int) (seq.extract s51 s14 s64))
(define-fun s66 () (Seq Int) (seq.++ s56 s65))
(define-fun s67 () (Seq Int) (seq.++ s35 s66))
(define-fun s68 () Bool (= s12 s65))
(define-fun s70 () (Seq Int) (seq.unit s69))
(define-fun s71 () Int (seq.len s65))
(define-fun s72 () Bool (> s71 s26))
(define-fun s73 () Bool (not s72))
(define-fun s74 () (Seq Int) (seq.extract s65 s26 s14))
(define-fun s75 () Bool (= s70 s74))
(define-fun s76 () Bool (or s73 s75))
(define-fun s77 () Bool (< s34 s69))
(define-fun s78 () Int (- s71 s14))
(define-fun s79 () (Seq Int) (seq.extract s65 s14 s78))
(define-fun s80 () (Seq Int) (seq.++ s70 s79))
(define-fun s81 () (Seq Int) (seq.++ s35 s80))
(define-fun s82 () (Seq Int) (seq.++ s70 s35))
(define-fun s83 () (Seq Int) (ite s77 s81 s82))
(define-fun s84 () (Seq Int) (ite s68 s35 s83))
(define-fun s85 () (Seq Int) (seq.++ s56 s84))
(define-fun s86 () (Seq Int) (ite s63 s67 s85))
(define-fun s87 () (Seq Int) (ite s54 s35 s86))
(define-fun s88 () (Seq Int) (seq.++ s42 s87))
(define-fun s89 () (Seq Int) (ite s49 s53 s88))
(define-fun s90 () (Seq Int) (ite s33 s35 s89))
(define-fun s91 () (Seq Int) (ite s18 s12 s90))
(define-fun s92 () Bool (= s12 s91))
(define-fun s94 () (Seq Int) (seq.unit s93))
(define-fun s95 () Bool (> s15 s26))
(define-fun s96 () Bool (not s95))
(define-fun s97 () (Seq Int) (seq.extract s11 s26 s14))
(define-fun s98 () Bool (= s94 s97))
(define-fun s99 () Bool (or s96 s98))
(define-fun s101 () (Seq Int) (seq.unit s100))
(define-fun s102 () Int (seq.len s91))
(define-fun s103 () Bool (> s102 s26))
(define-fun s104 () Bool (not s103))
(define-fun s105 () (Seq Int) (seq.extract s91 s26 s14))
(define-fun s106 () Bool (= s101 s105))
(define-fun s107 () Bool (or s104 s106))
(define-fun s108 () Bool (< s93 s100))
(define-fun s109 () Int (- s102 s14))
(define-fun s110 () (Seq Int) (seq.extract s91 s14 s109))
(define-fun s111 () (Seq Int) (seq.++ s101 s110))
(define-fun s112 () (Seq Int) (seq.++ s94 s111))
(define-fun s113 () Bool (= s12 s110))
(define-fun s115 () (Seq Int) (seq.unit s114))
(define-fun s116 () Int (seq.len s110))
(define-fun s117 () Bool (> s116 s26))
(define-fun s118 () Bool (not s117))
(define-fun s119 () (Seq Int) (seq.extract s110 s26 s14))
(define-fun s120 () Bool (= s115 s119))
(define-fun s121 () Bool (or s118 s120))
(define-fun s122 () Bool (< s93 s114))
(define-fun s123 () Int (- s116 s14))
(define-fun s124 () (Seq Int) (seq.extract s110 s14 s123))
(define-fun s125 () (Seq Int) (seq.++ s115 s124))
(define-fun s126 () (Seq Int) (seq.++ s94 s125))
(define-fun s127 () Bool (= s12 s124))
(define-fun s129 () (Seq Int) (seq.unit s128))
(define-fun s130 () Int (seq.len s124))
(define-fun s131 () Bool (> s130 s26))
(define-fun s132 () Bool (not s131))
(define-fun s133 () (Seq Int) (seq.extract s124 s26 s14))
(define-fun s134 () Bool (= s129 s133))
(define-fun s135 () Bool (or s132 s134))
(define-fun s136 () Bool (< s93 s128))
(define-fun s137 () Int (- s130 s14))
(define-fun s138 () (Seq Int) (seq.extract s124 s14 s137))
(define-fun s139 () (Seq Int) (seq.++ s129 s138))
(define-fun s140 () (Seq Int) (seq.++ s94 s139))
(define-fun s141 () (Seq Int) (seq.++ s129 s94))
(define-fun s142 () (Seq Int) (ite s136 s140 s141))
(define-fun s143 () (Seq Int) (ite s127 s94 s142))
(define-fun s144 () (Seq Int) (seq.++ s115 s143))
(define-fun s145 () (Seq Int) (ite s122 s126 s144))
(define-fun s146 () (Seq Int) (ite s113 s94 s145))
(define-fun s147 () (Seq Int) (seq.++ s101 s146))
(define-fun s148 () (Seq Int) (ite s108 s112 s147))
(define-fun s149 () (Seq Int) (ite s92 s94 s148))
(define-fun s150 () (Seq Int) (ite s13 s12 s149))
(define-fun s151 () Bool (= s11 s150))
(define-fun s152 () Bool (or s6 s151))
(define-fun s153 () Bool (<= s0 s2))
(define-fun s154 () Bool (<= s2 s1))
(define-fun s155 () Bool (and s153 s154))
(define-fun s156 () Bool (not s155))
(define-fun s157 () (Seq Int) (seq.++ s9 s8))
(define-fun s158 () (Seq Int) (seq.++ s7 s157))
(define-fun s159 () Bool (= s150 s158))
(define-fun s160 () Bool (or s156 s159))
(define-fun s161 () Bool (<= s1 s0))
(define-fun s162 () Bool (and s153 s161))
(define-fun s163 () Bool (not s162))
(define-fun s164 () (Seq Int) (seq.++ s7 s9))
(define-fun s165 () (Seq Int) (seq.++ s8 s164))
(define-fun s166 () Bool (= s150 s165))
(define-fun s167 () Bool (or s163 s166))
(define-fun s168 () Bool (<= s2 s0))
(define-fun s169 () Bool (and s4 s168))
(define-fun s170 () Bool (not s169))
(define-fun s171 () (Seq Int) (seq.++ s9 s7))
(define-fun s172 () (Seq Int) (seq.++ s8 s171))
(define-fun s173 () Bool (= s150 s172))
(define-fun s174 () Bool (or s170 s173))
(define-fun s175 () Bool (and s3 s168))
(define-fun s176 () Bool (not s175))
(define-fun s177 () (Seq Int) (seq.++ s7 s8))
(define-fun s178 () (Seq Int) (seq.++ s9 s177))
(define-fun s179 () Bool (= s150 s178))
(define-fun s180 () Bool (or s176 s179))
(define-fun s181 () Bool (and s154 s161))
(define-fun s182 () Bool (not s181))
(define-fun s183 () (Seq Int) (seq.++ s8 s7))
(define-fun s184 () (Seq Int) (seq.++ s9 s183))
(define-fun s185 () Bool (= s150 s184))
(define-fun s186 () Bool (or s182 s185))
(assert s31)
(assert s40)
(assert s48)
(assert s62)
(assert s76)
(assert s99)
(assert s107)
(assert s121)
(assert s135)
(assert s152)
(assert s160)
(assert s167)
(assert s174)
(assert s180)
(assert s186)
(check-sat)

[NikolajBjorner]

it is from a push today. looking at it. the sequence code is still churning a bit, but I don't have much more I want to change in this round.