** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-option :pp.max_depth      4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def  true      )
[GOOD] (set-logic ALL) ; has unbounded values, using catch-all.
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- ADTs  --- 
[GOOD] ; User defined ADT: Expr
[GOOD] (declare-datatype Expr (
           (Val (getVal_1 Int))
           (Var (getVar_1 String))
           (Add (getAdd_1 Expr) (getAdd_2 Expr))
           (Mul (getMul_1 Expr) (getMul_2 Expr))
           (Let (getLet_1 String) (getLet_2 Expr) (getLet_3 Expr))
       ))
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s15 () Expr ((as Val Expr) (- 5)))
[GOOD] (define-fun s17 () Expr ((as Val Expr) (- 4)))
[GOOD] (define-fun s19 () Expr ((as Val Expr) (- 3)))
[GOOD] (define-fun s21 () Expr ((as Val Expr) (- 2)))
[GOOD] (define-fun s23 () Expr ((as Val Expr) (- 1)))
[GOOD] (define-fun s25 () Expr ((as Val Expr) 0))
[GOOD] (define-fun s27 () Expr ((as Val Expr) 1))
[GOOD] (define-fun s29 () Expr ((as Val Expr) 2))
[GOOD] (define-fun s31 () Expr ((as Val Expr) 3))
[GOOD] (define-fun s33 () Expr ((as Val Expr) 4))
[GOOD] (define-fun s35 () Expr ((as Val Expr) 5))
[GOOD] (define-fun s37 () Expr ((as Val Expr) 6))
[GOOD] (define-fun s39 () Expr ((as Val Expr) 7))
[GOOD] (define-fun s41 () Expr ((as Val Expr) 8))
[GOOD] (define-fun s43 () Expr ((as Val Expr) 9))
[GOOD] (define-fun s61 () String "a")
[GOOD] (define-fun s64 () Int 0)
[GOOD] (define-fun s65 () String "b")
[GOOD] (define-fun s67 () String "c")
[GOOD] (define-fun s71 () Int 1)
[GOOD] (define-fun s72 () Int 2)
[GOOD] (define-fun s75 () Int 10)
[GOOD] (define-fun s78 () Int 3)
[GOOD] (define-fun s81 () Int 4)
[GOOD] (define-fun s84 () Int 5)
[GOOD] (define-fun s85 () Int 6)
[GOOD] (define-fun s414 () Int 45)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () Expr)
[GOOD] (declare-fun s1 () Expr)
[GOOD] (declare-fun s2 () Expr)
[GOOD] (declare-fun s3 () Expr)
[GOOD] (declare-fun s4 () Expr)
[GOOD] (declare-fun s5 () Expr)
[GOOD] (declare-fun s6 () Expr)
[GOOD] (declare-fun s7 () Expr)
[GOOD] (declare-fun s8 () Expr)
[GOOD] (declare-fun s9 () Expr)
[GOOD] (declare-fun s10 () Expr)
[GOOD] (declare-fun s11 () Expr)
[GOOD] (declare-fun s12 () Expr)
[GOOD] (declare-fun s13 () Expr)
[GOOD] (declare-fun s14 () Expr)
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s16 () Bool (= s0 s15))
[GOOD] (define-fun s18 () Bool (= s1 s17))
[GOOD] (define-fun s20 () Bool (= s2 s19))
[GOOD] (define-fun s22 () Bool (= s3 s21))
[GOOD] (define-fun s24 () Bool (= s4 s23))
[GOOD] (define-fun s26 () Bool (= s5 s25))
[GOOD] (define-fun s28 () Bool (= s6 s27))
[GOOD] (define-fun s30 () Bool (= s7 s29))
[GOOD] (define-fun s32 () Bool (= s8 s31))
[GOOD] (define-fun s34 () Bool (= s9 s33))
[GOOD] (define-fun s36 () Bool (= s10 s35))
[GOOD] (define-fun s38 () Bool (= s11 s37))
[GOOD] (define-fun s40 () Bool (= s12 s39))
[GOOD] (define-fun s42 () Bool (= s13 s41))
[GOOD] (define-fun s44 () Bool (= s14 s43))
[GOOD] (define-fun s45 () Bool (and s42 s44))
[GOOD] (define-fun s46 () Bool (and s40 s45))
[GOOD] (define-fun s47 () Bool (and s38 s46))
[GOOD] (define-fun s48 () Bool (and s36 s47))
[GOOD] (define-fun s49 () Bool (and s34 s48))
[GOOD] (define-fun s50 () Bool (and s32 s49))
[GOOD] (define-fun s51 () Bool (and s30 s50))
[GOOD] (define-fun s52 () Bool (and s28 s51))
[GOOD] (define-fun s53 () Bool (and s26 s52))
[GOOD] (define-fun s54 () Bool (and s24 s53))
[GOOD] (define-fun s55 () Bool (and s22 s54))
[GOOD] (define-fun s56 () Bool (and s20 s55))
[GOOD] (define-fun s57 () Bool (and s18 s56))
[GOOD] (define-fun s58 () Bool (and s16 s57))
[GOOD] (define-fun s59 () Bool ((as is-Var Bool) s0))
[GOOD] (define-fun s60 () String (getVar_1 s0))
[GOOD] (define-fun s62 () Bool (= s60 s61))
[GOOD] (define-fun s63 () Bool (and s59 s62))
[GOOD] (define-fun s66 () Bool (= s60 s65))
[GOOD] (define-fun s68 () Bool (= s60 s67))
[GOOD] (define-fun s69 () Bool (or s66 s68))
[GOOD] (define-fun s70 () Bool (and s59 s69))
[GOOD] (define-fun s73 () Bool ((as is-Val Bool) s0))
[GOOD] (define-fun s74 () Int (getVal_1 s0))
[GOOD] (define-fun s76 () Bool (< s74 s75))
[GOOD] (define-fun s77 () Bool (and s73 s76))
[GOOD] (define-fun s79 () Bool (= s74 s75))
[GOOD] (define-fun s80 () Bool (and s73 s79))
[GOOD] (define-fun s82 () Bool (> s74 s75))
[GOOD] (define-fun s83 () Bool (and s73 s82))
[GOOD] (define-fun s86 () Int (ite s83 s84 s85))
[GOOD] (define-fun s87 () Int (ite s80 s81 s86))
[GOOD] (define-fun s88 () Int (ite s77 s78 s87))
[GOOD] (define-fun s89 () Int (ite s59 s72 s88))
[GOOD] (define-fun s90 () Int (ite s70 s71 s89))
[GOOD] (define-fun s91 () Int (ite s63 s64 s90))
[GOOD] (define-fun s92 () Bool ((as is-Var Bool) s1))
[GOOD] (define-fun s93 () String (getVar_1 s1))
[GOOD] (define-fun s94 () Bool (= s61 s93))
[GOOD] (define-fun s95 () Bool (and s92 s94))
[GOOD] (define-fun s96 () Bool (= s65 s93))
[GOOD] (define-fun s97 () Bool (= s67 s93))
[GOOD] (define-fun s98 () Bool (or s96 s97))
[GOOD] (define-fun s99 () Bool (and s92 s98))
[GOOD] (define-fun s100 () Bool ((as is-Val Bool) s1))
[GOOD] (define-fun s101 () Int (getVal_1 s1))
[GOOD] (define-fun s102 () Bool (< s101 s75))
[GOOD] (define-fun s103 () Bool (and s100 s102))
[GOOD] (define-fun s104 () Bool (= s75 s101))
[GOOD] (define-fun s105 () Bool (and s100 s104))
[GOOD] (define-fun s106 () Bool (> s101 s75))
[GOOD] (define-fun s107 () Bool (and s100 s106))
[GOOD] (define-fun s108 () Int (ite s107 s84 s85))
[GOOD] (define-fun s109 () Int (ite s105 s81 s108))
[GOOD] (define-fun s110 () Int (ite s103 s78 s109))
[GOOD] (define-fun s111 () Int (ite s92 s72 s110))
[GOOD] (define-fun s112 () Int (ite s99 s71 s111))
[GOOD] (define-fun s113 () Int (ite s95 s64 s112))
[GOOD] (define-fun s114 () Int (+ s91 s113))
[GOOD] (define-fun s115 () Bool ((as is-Var Bool) s2))
[GOOD] (define-fun s116 () String (getVar_1 s2))
[GOOD] (define-fun s117 () Bool (= s61 s116))
[GOOD] (define-fun s118 () Bool (and s115 s117))
[GOOD] (define-fun s119 () Bool (= s65 s116))
[GOOD] (define-fun s120 () Bool (= s67 s116))
[GOOD] (define-fun s121 () Bool (or s119 s120))
[GOOD] (define-fun s122 () Bool (and s115 s121))
[GOOD] (define-fun s123 () Bool ((as is-Val Bool) s2))
[GOOD] (define-fun s124 () Int (getVal_1 s2))
[GOOD] (define-fun s125 () Bool (< s124 s75))
[GOOD] (define-fun s126 () Bool (and s123 s125))
[GOOD] (define-fun s127 () Bool (= s75 s124))
[GOOD] (define-fun s128 () Bool (and s123 s127))
[GOOD] (define-fun s129 () Bool (> s124 s75))
[GOOD] (define-fun s130 () Bool (and s123 s129))
[GOOD] (define-fun s131 () Int (ite s130 s84 s85))
[GOOD] (define-fun s132 () Int (ite s128 s81 s131))
[GOOD] (define-fun s133 () Int (ite s126 s78 s132))
[GOOD] (define-fun s134 () Int (ite s115 s72 s133))
[GOOD] (define-fun s135 () Int (ite s122 s71 s134))
[GOOD] (define-fun s136 () Int (ite s118 s64 s135))
[GOOD] (define-fun s137 () Int (+ s114 s136))
[GOOD] (define-fun s138 () Bool ((as is-Var Bool) s3))
[GOOD] (define-fun s139 () String (getVar_1 s3))
[GOOD] (define-fun s140 () Bool (= s61 s139))
[GOOD] (define-fun s141 () Bool (and s138 s140))
[GOOD] (define-fun s142 () Bool (= s65 s139))
[GOOD] (define-fun s143 () Bool (= s67 s139))
[GOOD] (define-fun s144 () Bool (or s142 s143))
[GOOD] (define-fun s145 () Bool (and s138 s144))
[GOOD] (define-fun s146 () Bool ((as is-Val Bool) s3))
[GOOD] (define-fun s147 () Int (getVal_1 s3))
[GOOD] (define-fun s148 () Bool (< s147 s75))
[GOOD] (define-fun s149 () Bool (and s146 s148))
[GOOD] (define-fun s150 () Bool (= s75 s147))
[GOOD] (define-fun s151 () Bool (and s146 s150))
[GOOD] (define-fun s152 () Bool (> s147 s75))
[GOOD] (define-fun s153 () Bool (and s146 s152))
[GOOD] (define-fun s154 () Int (ite s153 s84 s85))
[GOOD] (define-fun s155 () Int (ite s151 s81 s154))
[GOOD] (define-fun s156 () Int (ite s149 s78 s155))
[GOOD] (define-fun s157 () Int (ite s138 s72 s156))
[GOOD] (define-fun s158 () Int (ite s145 s71 s157))
[GOOD] (define-fun s159 () Int (ite s141 s64 s158))
[GOOD] (define-fun s160 () Int (+ s137 s159))
[GOOD] (define-fun s161 () Bool ((as is-Var Bool) s4))
[GOOD] (define-fun s162 () String (getVar_1 s4))
[GOOD] (define-fun s163 () Bool (= s61 s162))
[GOOD] (define-fun s164 () Bool (and s161 s163))
[GOOD] (define-fun s165 () Bool (= s65 s162))
[GOOD] (define-fun s166 () Bool (= s67 s162))
[GOOD] (define-fun s167 () Bool (or s165 s166))
[GOOD] (define-fun s168 () Bool (and s161 s167))
[GOOD] (define-fun s169 () Bool ((as is-Val Bool) s4))
[GOOD] (define-fun s170 () Int (getVal_1 s4))
[GOOD] (define-fun s171 () Bool (< s170 s75))
[GOOD] (define-fun s172 () Bool (and s169 s171))
[GOOD] (define-fun s173 () Bool (= s75 s170))
[GOOD] (define-fun s174 () Bool (and s169 s173))
[GOOD] (define-fun s175 () Bool (> s170 s75))
[GOOD] (define-fun s176 () Bool (and s169 s175))
[GOOD] (define-fun s177 () Int (ite s176 s84 s85))
[GOOD] (define-fun s178 () Int (ite s174 s81 s177))
[GOOD] (define-fun s179 () Int (ite s172 s78 s178))
[GOOD] (define-fun s180 () Int (ite s161 s72 s179))
[GOOD] (define-fun s181 () Int (ite s168 s71 s180))
[GOOD] (define-fun s182 () Int (ite s164 s64 s181))
[GOOD] (define-fun s183 () Int (+ s160 s182))
[GOOD] (define-fun s184 () Bool ((as is-Var Bool) s5))
[GOOD] (define-fun s185 () String (getVar_1 s5))
[GOOD] (define-fun s186 () Bool (= s61 s185))
[GOOD] (define-fun s187 () Bool (and s184 s186))
[GOOD] (define-fun s188 () Bool (= s65 s185))
[GOOD] (define-fun s189 () Bool (= s67 s185))
[GOOD] (define-fun s190 () Bool (or s188 s189))
[GOOD] (define-fun s191 () Bool (and s184 s190))
[GOOD] (define-fun s192 () Bool ((as is-Val Bool) s5))
[GOOD] (define-fun s193 () Int (getVal_1 s5))
[GOOD] (define-fun s194 () Bool (< s193 s75))
[GOOD] (define-fun s195 () Bool (and s192 s194))
[GOOD] (define-fun s196 () Bool (= s75 s193))
[GOOD] (define-fun s197 () Bool (and s192 s196))
[GOOD] (define-fun s198 () Bool (> s193 s75))
[GOOD] (define-fun s199 () Bool (and s192 s198))
[GOOD] (define-fun s200 () Int (ite s199 s84 s85))
[GOOD] (define-fun s201 () Int (ite s197 s81 s200))
[GOOD] (define-fun s202 () Int (ite s195 s78 s201))
[GOOD] (define-fun s203 () Int (ite s184 s72 s202))
[GOOD] (define-fun s204 () Int (ite s191 s71 s203))
[GOOD] (define-fun s205 () Int (ite s187 s64 s204))
[GOOD] (define-fun s206 () Int (+ s183 s205))
[GOOD] (define-fun s207 () Bool ((as is-Var Bool) s6))
[GOOD] (define-fun s208 () String (getVar_1 s6))
[GOOD] (define-fun s209 () Bool (= s61 s208))
[GOOD] (define-fun s210 () Bool (and s207 s209))
[GOOD] (define-fun s211 () Bool (= s65 s208))
[GOOD] (define-fun s212 () Bool (= s67 s208))
[GOOD] (define-fun s213 () Bool (or s211 s212))
[GOOD] (define-fun s214 () Bool (and s207 s213))
[GOOD] (define-fun s215 () Bool ((as is-Val Bool) s6))
[GOOD] (define-fun s216 () Int (getVal_1 s6))
[GOOD] (define-fun s217 () Bool (< s216 s75))
[GOOD] (define-fun s218 () Bool (and s215 s217))
[GOOD] (define-fun s219 () Bool (= s75 s216))
[GOOD] (define-fun s220 () Bool (and s215 s219))
[GOOD] (define-fun s221 () Bool (> s216 s75))
[GOOD] (define-fun s222 () Bool (and s215 s221))
[GOOD] (define-fun s223 () Int (ite s222 s84 s85))
[GOOD] (define-fun s224 () Int (ite s220 s81 s223))
[GOOD] (define-fun s225 () Int (ite s218 s78 s224))
[GOOD] (define-fun s226 () Int (ite s207 s72 s225))
[GOOD] (define-fun s227 () Int (ite s214 s71 s226))
[GOOD] (define-fun s228 () Int (ite s210 s64 s227))
[GOOD] (define-fun s229 () Int (+ s206 s228))
[GOOD] (define-fun s230 () Bool ((as is-Var Bool) s7))
[GOOD] (define-fun s231 () String (getVar_1 s7))
[GOOD] (define-fun s232 () Bool (= s61 s231))
[GOOD] (define-fun s233 () Bool (and s230 s232))
[GOOD] (define-fun s234 () Bool (= s65 s231))
[GOOD] (define-fun s235 () Bool (= s67 s231))
[GOOD] (define-fun s236 () Bool (or s234 s235))
[GOOD] (define-fun s237 () Bool (and s230 s236))
[GOOD] (define-fun s238 () Bool ((as is-Val Bool) s7))
[GOOD] (define-fun s239 () Int (getVal_1 s7))
[GOOD] (define-fun s240 () Bool (< s239 s75))
[GOOD] (define-fun s241 () Bool (and s238 s240))
[GOOD] (define-fun s242 () Bool (= s75 s239))
[GOOD] (define-fun s243 () Bool (and s238 s242))
[GOOD] (define-fun s244 () Bool (> s239 s75))
[GOOD] (define-fun s245 () Bool (and s238 s244))
[GOOD] (define-fun s246 () Int (ite s245 s84 s85))
[GOOD] (define-fun s247 () Int (ite s243 s81 s246))
[GOOD] (define-fun s248 () Int (ite s241 s78 s247))
[GOOD] (define-fun s249 () Int (ite s230 s72 s248))
[GOOD] (define-fun s250 () Int (ite s237 s71 s249))
[GOOD] (define-fun s251 () Int (ite s233 s64 s250))
[GOOD] (define-fun s252 () Int (+ s229 s251))
[GOOD] (define-fun s253 () Bool ((as is-Var Bool) s8))
[GOOD] (define-fun s254 () String (getVar_1 s8))
[GOOD] (define-fun s255 () Bool (= s61 s254))
[GOOD] (define-fun s256 () Bool (and s253 s255))
[GOOD] (define-fun s257 () Bool (= s65 s254))
[GOOD] (define-fun s258 () Bool (= s67 s254))
[GOOD] (define-fun s259 () Bool (or s257 s258))
[GOOD] (define-fun s260 () Bool (and s253 s259))
[GOOD] (define-fun s261 () Bool ((as is-Val Bool) s8))
[GOOD] (define-fun s262 () Int (getVal_1 s8))
[GOOD] (define-fun s263 () Bool (< s262 s75))
[GOOD] (define-fun s264 () Bool (and s261 s263))
[GOOD] (define-fun s265 () Bool (= s75 s262))
[GOOD] (define-fun s266 () Bool (and s261 s265))
[GOOD] (define-fun s267 () Bool (> s262 s75))
[GOOD] (define-fun s268 () Bool (and s261 s267))
[GOOD] (define-fun s269 () Int (ite s268 s84 s85))
[GOOD] (define-fun s270 () Int (ite s266 s81 s269))
[GOOD] (define-fun s271 () Int (ite s264 s78 s270))
[GOOD] (define-fun s272 () Int (ite s253 s72 s271))
[GOOD] (define-fun s273 () Int (ite s260 s71 s272))
[GOOD] (define-fun s274 () Int (ite s256 s64 s273))
[GOOD] (define-fun s275 () Int (+ s252 s274))
[GOOD] (define-fun s276 () Bool ((as is-Var Bool) s9))
[GOOD] (define-fun s277 () String (getVar_1 s9))
[GOOD] (define-fun s278 () Bool (= s61 s277))
[GOOD] (define-fun s279 () Bool (and s276 s278))
[GOOD] (define-fun s280 () Bool (= s65 s277))
[GOOD] (define-fun s281 () Bool (= s67 s277))
[GOOD] (define-fun s282 () Bool (or s280 s281))
[GOOD] (define-fun s283 () Bool (and s276 s282))
[GOOD] (define-fun s284 () Bool ((as is-Val Bool) s9))
[GOOD] (define-fun s285 () Int (getVal_1 s9))
[GOOD] (define-fun s286 () Bool (< s285 s75))
[GOOD] (define-fun s287 () Bool (and s284 s286))
[GOOD] (define-fun s288 () Bool (= s75 s285))
[GOOD] (define-fun s289 () Bool (and s284 s288))
[GOOD] (define-fun s290 () Bool (> s285 s75))
[GOOD] (define-fun s291 () Bool (and s284 s290))
[GOOD] (define-fun s292 () Int (ite s291 s84 s85))
[GOOD] (define-fun s293 () Int (ite s289 s81 s292))
[GOOD] (define-fun s294 () Int (ite s287 s78 s293))
[GOOD] (define-fun s295 () Int (ite s276 s72 s294))
[GOOD] (define-fun s296 () Int (ite s283 s71 s295))
[GOOD] (define-fun s297 () Int (ite s279 s64 s296))
[GOOD] (define-fun s298 () Int (+ s275 s297))
[GOOD] (define-fun s299 () Bool ((as is-Var Bool) s10))
[GOOD] (define-fun s300 () String (getVar_1 s10))
[GOOD] (define-fun s301 () Bool (= s61 s300))
[GOOD] (define-fun s302 () Bool (and s299 s301))
[GOOD] (define-fun s303 () Bool (= s65 s300))
[GOOD] (define-fun s304 () Bool (= s67 s300))
[GOOD] (define-fun s305 () Bool (or s303 s304))
[GOOD] (define-fun s306 () Bool (and s299 s305))
[GOOD] (define-fun s307 () Bool ((as is-Val Bool) s10))
[GOOD] (define-fun s308 () Int (getVal_1 s10))
[GOOD] (define-fun s309 () Bool (< s308 s75))
[GOOD] (define-fun s310 () Bool (and s307 s309))
[GOOD] (define-fun s311 () Bool (= s75 s308))
[GOOD] (define-fun s312 () Bool (and s307 s311))
[GOOD] (define-fun s313 () Bool (> s308 s75))
[GOOD] (define-fun s314 () Bool (and s307 s313))
[GOOD] (define-fun s315 () Int (ite s314 s84 s85))
[GOOD] (define-fun s316 () Int (ite s312 s81 s315))
[GOOD] (define-fun s317 () Int (ite s310 s78 s316))
[GOOD] (define-fun s318 () Int (ite s299 s72 s317))
[GOOD] (define-fun s319 () Int (ite s306 s71 s318))
[GOOD] (define-fun s320 () Int (ite s302 s64 s319))
[GOOD] (define-fun s321 () Int (+ s298 s320))
[GOOD] (define-fun s322 () Bool ((as is-Var Bool) s11))
[GOOD] (define-fun s323 () String (getVar_1 s11))
[GOOD] (define-fun s324 () Bool (= s61 s323))
[GOOD] (define-fun s325 () Bool (and s322 s324))
[GOOD] (define-fun s326 () Bool (= s65 s323))
[GOOD] (define-fun s327 () Bool (= s67 s323))
[GOOD] (define-fun s328 () Bool (or s326 s327))
[GOOD] (define-fun s329 () Bool (and s322 s328))
[GOOD] (define-fun s330 () Bool ((as is-Val Bool) s11))
[GOOD] (define-fun s331 () Int (getVal_1 s11))
[GOOD] (define-fun s332 () Bool (< s331 s75))
[GOOD] (define-fun s333 () Bool (and s330 s332))
[GOOD] (define-fun s334 () Bool (= s75 s331))
[GOOD] (define-fun s335 () Bool (and s330 s334))
[GOOD] (define-fun s336 () Bool (> s331 s75))
[GOOD] (define-fun s337 () Bool (and s330 s336))
[GOOD] (define-fun s338 () Int (ite s337 s84 s85))
[GOOD] (define-fun s339 () Int (ite s335 s81 s338))
[GOOD] (define-fun s340 () Int (ite s333 s78 s339))
[GOOD] (define-fun s341 () Int (ite s322 s72 s340))
[GOOD] (define-fun s342 () Int (ite s329 s71 s341))
[GOOD] (define-fun s343 () Int (ite s325 s64 s342))
[GOOD] (define-fun s344 () Int (+ s321 s343))
[GOOD] (define-fun s345 () Bool ((as is-Var Bool) s12))
[GOOD] (define-fun s346 () String (getVar_1 s12))
[GOOD] (define-fun s347 () Bool (= s61 s346))
[GOOD] (define-fun s348 () Bool (and s345 s347))
[GOOD] (define-fun s349 () Bool (= s65 s346))
[GOOD] (define-fun s350 () Bool (= s67 s346))
[GOOD] (define-fun s351 () Bool (or s349 s350))
[GOOD] (define-fun s352 () Bool (and s345 s351))
[GOOD] (define-fun s353 () Bool ((as is-Val Bool) s12))
[GOOD] (define-fun s354 () Int (getVal_1 s12))
[GOOD] (define-fun s355 () Bool (< s354 s75))
[GOOD] (define-fun s356 () Bool (and s353 s355))
[GOOD] (define-fun s357 () Bool (= s75 s354))
[GOOD] (define-fun s358 () Bool (and s353 s357))
[GOOD] (define-fun s359 () Bool (> s354 s75))
[GOOD] (define-fun s360 () Bool (and s353 s359))
[GOOD] (define-fun s361 () Int (ite s360 s84 s85))
[GOOD] (define-fun s362 () Int (ite s358 s81 s361))
[GOOD] (define-fun s363 () Int (ite s356 s78 s362))
[GOOD] (define-fun s364 () Int (ite s345 s72 s363))
[GOOD] (define-fun s365 () Int (ite s352 s71 s364))
[GOOD] (define-fun s366 () Int (ite s348 s64 s365))
[GOOD] (define-fun s367 () Int (+ s344 s366))
[GOOD] (define-fun s368 () Bool ((as is-Var Bool) s13))
[GOOD] (define-fun s369 () String (getVar_1 s13))
[GOOD] (define-fun s370 () Bool (= s61 s369))
[GOOD] (define-fun s371 () Bool (and s368 s370))
[GOOD] (define-fun s372 () Bool (= s65 s369))
[GOOD] (define-fun s373 () Bool (= s67 s369))
[GOOD] (define-fun s374 () Bool (or s372 s373))
[GOOD] (define-fun s375 () Bool (and s368 s374))
[GOOD] (define-fun s376 () Bool ((as is-Val Bool) s13))
[GOOD] (define-fun s377 () Int (getVal_1 s13))
[GOOD] (define-fun s378 () Bool (< s377 s75))
[GOOD] (define-fun s379 () Bool (and s376 s378))
[GOOD] (define-fun s380 () Bool (= s75 s377))
[GOOD] (define-fun s381 () Bool (and s376 s380))
[GOOD] (define-fun s382 () Bool (> s377 s75))
[GOOD] (define-fun s383 () Bool (and s376 s382))
[GOOD] (define-fun s384 () Int (ite s383 s84 s85))
[GOOD] (define-fun s385 () Int (ite s381 s81 s384))
[GOOD] (define-fun s386 () Int (ite s379 s78 s385))
[GOOD] (define-fun s387 () Int (ite s368 s72 s386))
[GOOD] (define-fun s388 () Int (ite s375 s71 s387))
[GOOD] (define-fun s389 () Int (ite s371 s64 s388))
[GOOD] (define-fun s390 () Int (+ s367 s389))
[GOOD] (define-fun s391 () Bool ((as is-Var Bool) s14))
[GOOD] (define-fun s392 () String (getVar_1 s14))
[GOOD] (define-fun s393 () Bool (= s61 s392))
[GOOD] (define-fun s394 () Bool (and s391 s393))
[GOOD] (define-fun s395 () Bool (= s65 s392))
[GOOD] (define-fun s396 () Bool (= s67 s392))
[GOOD] (define-fun s397 () Bool (or s395 s396))
[GOOD] (define-fun s398 () Bool (and s391 s397))
[GOOD] (define-fun s399 () Bool ((as is-Val Bool) s14))
[GOOD] (define-fun s400 () Int (getVal_1 s14))
[GOOD] (define-fun s401 () Bool (< s400 s75))
[GOOD] (define-fun s402 () Bool (and s399 s401))
[GOOD] (define-fun s403 () Bool (= s75 s400))
[GOOD] (define-fun s404 () Bool (and s399 s403))
[GOOD] (define-fun s405 () Bool (> s400 s75))
[GOOD] (define-fun s406 () Bool (and s399 s405))
[GOOD] (define-fun s407 () Int (ite s406 s84 s85))
[GOOD] (define-fun s408 () Int (ite s404 s81 s407))
[GOOD] (define-fun s409 () Int (ite s402 s78 s408))
[GOOD] (define-fun s410 () Int (ite s391 s72 s409))
[GOOD] (define-fun s411 () Int (ite s398 s71 s410))
[GOOD] (define-fun s412 () Int (ite s394 s64 s411))
[GOOD] (define-fun s413 () Int (+ s390 s412))
[GOOD] (define-fun s415 () Bool (distinct s413 s414))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert s58)
[GOOD] (assert s415)
[SEND] (check-sat)
[RECV] unsat
All good.
*** Solver   : Z3
*** Exit code: ExitSuccess