Skip to content

Instantly share code, notes, and snippets.

@abakst

abakst/bad.smt

Last active July 8, 2020 17:52
Show Gist options
  • Save abakst/7a46062e67a581824843393b3f771787 to your computer and use it in GitHub Desktop.
Save abakst/7a46062e67a581824843393b3f771787 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
bad.smt
; No segfault if the below line is uncommented
;(set-option :produce-proofs true)
;
; success
(set-option :produce-models true)
; success
(set-option :pp.decimal true)
; success
(set-option :global-declarations true)
; success
(set-option :produce-unsat-cores true)
; success
(get-info :error-behavior)
; (:error-behavior continued-execution)
(push 1)
; success
(push 1)
; success
(declare-fun x!0 () (_ BitVec 32))
; success
(define-fun x!1 () Bool (bvslt x!0 (_ bv0 32)))
; success
(declare-fun x!2 () (_ BitVec 32))
; success
(define-fun x!3 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!2) (_ bv2147483648 32)))
; success
(define-fun x!4 () (_ BitVec 32) (ite x!1 x!3 (_ bv0 32)))
; success
(define-fun x!5 () Bool (bvslt x!4 (_ bv0 32)))
; success
(define-fun x!6 () Bool (not x!5))
; success
(assert x!6)
; success
(declare-fun x!7 () (_ BitVec 32))
; success
(declare-fun x!8 () (_ BitVec 32))
; success
(define-fun x!9 () Bool (= x!7 x!8))
; success
(assert x!9)
; success
(declare-fun x!10 () (_ BitVec 32))
; success
(define-fun x!11 () Bool (= (_ bv5 32) x!10))
; success
(assert x!11)
; success
(declare-fun x!12 () (_ BitVec 32))
; success
(define-fun x!13 () Bool (= x!7 x!12))
; success
(assert x!13)
; success
(declare-fun x!14 () (_ BitVec 32))
; success
(define-fun x!15 () Bool (= (_ bv5 32) x!14))
; success
(assert x!15)
; success
(declare-fun x!16 () (_ BitVec 32))
; success
(define-fun x!17 () Bool (= x!7 x!16))
; success
(assert x!17)
; success
(declare-fun x!18 () (_ BitVec 32))
; success
(define-fun x!19 () Bool (= (_ bv5 32) x!18))
; success
(assert x!19)
; success
(declare-fun x!20 () (_ BitVec 32))
; success
(define-fun x!21 () Bool (= x!7 x!20))
; success
(assert x!21)
; success
(declare-fun x!22 () (_ BitVec 32))
; success
(define-fun x!23 () Bool (= (_ bv5 32) x!22))
; success
(assert x!23)
; success
(pop 1)
; success
(push 1)
; success
(define-fun x!24 () Bool (bvslt x!0 (_ bv0 32)))
; success
(define-fun x!25 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!2) (_ bv2147483648 32)))
; success
(define-fun x!26 () (_ BitVec 32) (ite x!24 x!25 (_ bv0 32)))
; success
(define-fun x!27 () Bool (bvslt x!26 (_ bv0 32)))
; success
(assert x!27)
; success
(pop 1)
; success
(define-fun x!28 () Bool (bvslt x!0 (_ bv0 32)))
; success
(define-fun x!29 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!2) (_ bv2147483648 32)))
; success
(define-fun x!30 () (_ BitVec 32) (ite x!28 x!29 (_ bv0 32)))
; success
(define-fun x!31 () Bool (bvslt x!30 (_ bv0 32)))
; success
(define-fun x!32 () Bool (= x!7 x!8))
; success
(define-fun x!33 () Bool (and (not x!31) (not x!32)))
; success
(define-fun x!34 () Bool (not x!33))
; success
(assert x!34)
; success
(define-fun x!35 () Bool (= (_ bv5 32) x!10))
; success
(define-fun x!36 () Bool (and (not x!31) (not x!35)))
; success
(define-fun x!37 () Bool (not x!36))
; success
(assert x!37)
; success
(define-fun x!38 () Bool (= x!7 x!12))
; success
(define-fun x!39 () Bool (and (not x!31) (not x!38)))
; success
(define-fun x!40 () Bool (not x!39))
; success
(assert x!40)
; success
(define-fun x!41 () Bool (= (_ bv5 32) x!14))
; success
(define-fun x!42 () Bool (and (not x!31) (not x!41)))
; success
(define-fun x!43 () Bool (not x!42))
; success
(assert x!43)
; success
(define-fun x!44 () Bool (= x!7 x!16))
; success
(define-fun x!45 () Bool (and (not x!31) (not x!44)))
; success
(define-fun x!46 () Bool (not x!45))
; success
(assert x!46)
; success
(define-fun x!47 () Bool (= (_ bv5 32) x!18))
; success
(define-fun x!48 () Bool (and (not x!31) (not x!47)))
; success
(define-fun x!49 () Bool (not x!48))
; success
(assert x!49)
; success
(define-fun x!50 () Bool (= x!7 x!20))
; success
(define-fun x!51 () Bool (and (not x!31) (not x!50)))
; success
(define-fun x!52 () Bool (not x!51))
; success
(assert x!52)
; success
(define-fun x!53 () Bool (= (_ bv5 32) x!22))
; success
(define-fun x!54 () Bool (and (not x!31) (not x!53)))
; success
(define-fun x!55 () Bool (not x!54))
; success
(assert x!55)
; success
(push 1)
; success
(declare-fun x!56 () (_ BitVec 32))
; success
(define-fun x!57 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!56) (_ bv2147483648 32)))
; success
(define-fun x!58 () (_ BitVec 32) (ite x!28 x!57 (_ bv0 32)))
; success
(declare-fun x!59 () (_ BitVec 32))
; success
(define-fun x!60 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!59) (_ bv2147483648 32)))
; success
(define-fun x!61 () (_ BitVec 32) (ite x!28 x!60 (_ bv0 32)))
; success
(define-fun x!62 () (_ BitVec 32) (ite x!31 x!58 x!61))
; success
(define-fun x!63 () Bool (bvslt x!62 (_ bv0 32)))
; success
(define-fun x!64 () Bool (not x!63))
; success
(assert x!64)
; success
(declare-fun x!65 () (_ BitVec 32))
; success
(define-fun x!66 () Bool (= x!7 x!65))
; success
(assert x!66)
; success
(push 1)
; success
(define-fun x!67 () Bool (not x!28))
; success
(define-fun x!68 () Bool (not x!28))
; success
(define-fun x!69 () Bool (ite x!31 x!67 x!68))
; success
(assert x!69)
; success
(pop 1)
; success
(push 1)
; success
(define-fun x!70 () Bool (not x!28))
; success
(define-fun x!71 () Bool (not x!28))
; success
(define-fun x!72 () Bool (ite x!31 x!70 x!71))
; success
(define-fun x!73 () Bool (not x!72))
; success
(assert x!73)
; success
(pop 1)
; success
(define-fun x!74 () Bool (not x!28))
; success
(define-fun x!75 () Bool (not x!28))
; success
(define-fun x!76 () Bool (ite x!31 x!74 x!75))
; success
(assert x!76)
; success
(declare-fun x!77 () (_ BitVec 32))
; success
(define-fun x!78 () Bool (= x!7 x!77))
; success
(assert x!78)
; success
(declare-fun x!79 () (_ BitVec 32))
; success
(define-fun x!80 () Bool (= x!7 x!79))
; success
(assert x!80)
; success
(pop 1)
; success
(push 1)
; success
(define-fun x!81 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!56) (_ bv2147483648 32)))
; success
(define-fun x!82 () (_ BitVec 32) (ite x!28 x!81 (_ bv0 32)))
; success
(define-fun x!83 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!59) (_ bv2147483648 32)))
; success
(define-fun x!84 () (_ BitVec 32) (ite x!28 x!83 (_ bv0 32)))
; success
(define-fun x!85 () (_ BitVec 32) (ite x!31 x!82 x!84))
; success
(define-fun x!86 () Bool (bvslt x!85 (_ bv0 32)))
; success
(assert x!86)
; success
(pop 1)
; success
(define-fun x!87 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!56) (_ bv2147483648 32)))
; success
(define-fun x!88 () (_ BitVec 32) (ite x!28 x!87 (_ bv0 32)))
; success
(define-fun x!89 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!59) (_ bv2147483648 32)))
; success
(define-fun x!90 () (_ BitVec 32) (ite x!28 x!89 (_ bv0 32)))
; success
(define-fun x!91 () (_ BitVec 32) (ite x!31 x!88 x!90))
; success
(define-fun x!92 () Bool (bvslt x!91 (_ bv0 32)))
; success
(define-fun x!93 () Bool (= x!7 x!65))
; success
(define-fun x!94 () Bool (and (not x!92) (not x!93)))
; success
(define-fun x!95 () Bool (not x!94))
; success
(assert x!95)
; success
(define-fun x!96 () Bool (not x!28))
; success
(define-fun x!97 () Bool (not x!28))
; success
(define-fun x!98 () Bool (ite x!31 x!96 x!97))
; success
(define-fun x!99 () Bool (and (not x!92) (not x!98)))
; success
(define-fun x!100 () Bool (not x!99))
; success
(assert x!100)
; success
(define-fun x!101 () Bool (= x!7 x!77))
; success
(define-fun x!102 () Bool (and (not x!92) (not x!101)))
; success
(define-fun x!103 () Bool (not x!102))
; success
(assert x!103)
; success
(define-fun x!104 () Bool (= x!7 x!79))
; success
(define-fun x!105 () Bool (and (not x!92) (not x!104)))
; success
(define-fun x!106 () Bool (not x!105))
; success
(assert x!106)
; success
(push 1)
; success
(declare-fun x!107 () (_ BitVec 32))
; success
(define-fun x!108 () Bool (bvslt x!107 (_ bv0 32)))
; success
(declare-fun x!109 () (_ BitVec 32))
; success
(define-fun x!110 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!109) (_ bv2147483648 32)))
; success
(define-fun x!111 () (_ BitVec 32) (ite x!108 x!110 (_ bv1 32)))
; success
(define-fun x!112 () Bool (bvslt x!111 (_ bv0 32)))
; success
(define-fun x!113 () Bool (not x!112))
; success
(assert x!113)
; success
(declare-datatypes (T0 T1 T2 T3) ((Struct4 (mk-struct4 (struct4-proj0 T0) (struct4-proj1 T1) (struct4-proj2 T2) (struct4-proj3 T3)))))
; success
(declare-fun x!114 () (Array (_ BitVec 32) (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)))))
; success
(declare-fun x!115 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))))
; success
(define-fun x!116 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) RNE 0.0))
; success
(define-fun x!117 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (mk-struct4 (_ bv0 32) (_ bv0 32) (_ bv0 32) x!116))
; success
(define-fun x!118 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store x!115 (_ bv0 32) x!117) (_ bv1 32) x!117) (_ bv2 32) x!117) (_ bv3 32) x!117) (_ bv4 32) x!117) (_ bv5 32) x!117) (_ bv6 32) x!117) (_ bv7 32) x!117) (_ bv8 32) x!117) (_ bv9 32) x!117) (_ bv10 32) x!117) (_ bv11 32) x!117) (_ bv12 32) x!117) (_ bv13 32) x!117) (_ bv14 32) x!117) (_ bv15 32) x!117))
; success
(define-fun x!119 () (Array (_ BitVec 32) (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)))) (store x!114 (_ bv1 32) x!118))
; success
(declare-fun x!120 () (_ BitVec 32))
; success
(define-fun x!121 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!120) (_ bv2147483648 32)))
; success
(define-fun x!122 () (_ BitVec 32) (ite x!108 x!121 (_ bv1 32)))
; success
(define-fun x!123 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (select x!119 x!122))
; success
(define-fun x!124 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (select x!123 (_ bv0 32)))
; success
(define-fun x!125 () (_ BitVec 32) (struct4-proj1 x!124))
; success
(define-fun x!126 () Bool (= (_ bv0 32) x!125))
; success
(define-fun x!127 () Bool (= (_ bv4 32) x!125))
; success
(define-fun x!128 () (_ BitVec 32) (struct4-proj0 x!124))
; success
(define-fun x!129 () Bool (= (_ bv0 32) x!128))
; success
(define-fun x!130 () Bool (and x!127 x!129))
; success
(define-fun x!131 () Bool (and (not x!126) (not x!130)))
; success
(assert (not x!131))
; success
(define-fun x!132 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (select x!123 (_ bv1 32)))
; success
(define-fun x!133 () (_ BitVec 32) (struct4-proj1 x!132))
; success
(define-fun x!134 () Bool (= (_ bv0 32) x!133))
; success
(define-fun x!135 () Bool (= (_ bv4 32) x!133))
; success
(define-fun x!136 () (_ BitVec 32) (struct4-proj0 x!132))
; success
(define-fun x!137 () Bool (= (_ bv0 32) x!136))
; success
(define-fun x!138 () Bool (and x!135 x!137))
; success
(define-fun x!139 () Bool (and (not x!134) (not x!138)))
; success
(assert (not x!139))
; success
(define-fun x!140 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (select x!123 (_ bv2 32)))
; success
(define-fun x!141 () (_ BitVec 32) (struct4-proj1 x!140))
; success
(define-fun x!142 () Bool (= (_ bv0 32) x!141))
; success
(define-fun x!143 () Bool (= (_ bv4 32) x!141))
; success
(define-fun x!144 () (_ BitVec 32) (struct4-proj0 x!140))
; success
(define-fun x!145 () Bool (= (_ bv0 32) x!144))
; success
(define-fun x!146 () Bool (and x!143 x!145))
; success
(define-fun x!147 () Bool (and (not x!142) (not x!146)))
; success
(assert (not x!147))
; success
(define-fun x!148 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (select x!123 (_ bv3 32)))
; success
(define-fun x!149 () (_ BitVec 32) (struct4-proj1 x!148))
; success
(define-fun x!150 () Bool (= (_ bv0 32) x!149))
; success
(define-fun x!151 () Bool (= (_ bv4 32) x!149))
; success
(define-fun x!152 () (_ BitVec 32) (struct4-proj0 x!148))
; success
(define-fun x!153 () Bool (= (_ bv0 32) x!152))
; success
(define-fun x!154 () Bool (and x!151 x!153))
; success
(define-fun x!155 () Bool (and (not x!150) (not x!154)))
; success
(assert (not x!155))
; success
(declare-fun x!156 () (Array (_ BitVec 32) (_ BitVec 32)))
; success
(define-fun x!157 () (Array (_ BitVec 32) (_ BitVec 32)) (store (store x!156 (_ bv0 32) (_ bv16 32)) (_ bv1 32) (_ bv16 32)))
; success
(declare-fun x!158 () (_ BitVec 32))
; success
(define-fun x!159 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!158) (_ bv2147483648 32)))
; success
(define-fun x!160 () (_ BitVec 32) (ite x!108 x!159 (_ bv1 32)))
; success
(define-fun x!161 () (_ BitVec 32) (select x!157 x!160))
; success
(define-fun x!162 () Bool (bvult (_ bv0 32) x!161))
; success
(assert x!162)
; success
(define-fun x!163 () Bool (bvult x!161 (_ bv4 32)))
; success
(assert (not x!163))
; success
(declare-fun x!164 () (_ BitVec 32))
; success
(define-fun x!165 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!164) (_ bv2147483648 32)))
; success
(define-fun x!166 () (_ BitVec 32) (ite x!108 x!165 (_ bv1 32)))
; success
(define-fun x!167 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (select x!119 x!166))
; success
(declare-fun x!168 () (_ FloatingPoint 8 24))
; success
(define-fun x!169 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (mk-struct4 (_ bv0 32) (_ bv4 32) (_ bv5 32) x!168))
; success
(define-fun x!170 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (store x!167 (_ bv0 32) x!169))
; success
(define-fun x!171 () (Array (_ BitVec 32) (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)))) (store x!119 x!166 x!170))
; success
(define-fun x!172 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (select x!171 x!166))
; success
(define-fun x!173 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (store x!172 (_ bv1 32) x!169))
; success
(define-fun x!174 () (Array (_ BitVec 32) (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)))) (store x!171 x!166 x!173))
; success
(define-fun x!175 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (select x!174 x!166))
; success
(define-fun x!176 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (store x!175 (_ bv2 32) x!169))
; success
(define-fun x!177 () (Array (_ BitVec 32) (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)))) (store x!174 x!166 x!176))
; success
(define-fun x!178 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (select x!177 x!166))
; success
(define-fun x!179 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (store x!178 (_ bv3 32) x!169))
; success
(define-fun x!180 () (Array (_ BitVec 32) (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)))) (store x!177 x!166 x!179))
; success
(declare-fun x!181 () (_ BitVec 32))
; success
(define-fun x!182 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!181) (_ bv2147483648 32)))
; success
(define-fun x!183 () (_ BitVec 32) (ite x!108 x!182 (_ bv1 32)))
; success
(define-fun x!184 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (select x!180 x!183))
; success
(define-fun x!185 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (select x!184 (_ bv4 32)))
; success
(define-fun x!186 () (_ BitVec 32) (struct4-proj1 x!185))
; success
(define-fun x!187 () Bool (= (_ bv0 32) x!186))
; success
(define-fun x!188 () Bool (= (_ bv4 32) x!186))
; success
(define-fun x!189 () (_ BitVec 32) (struct4-proj0 x!185))
; success
(define-fun x!190 () Bool (= (_ bv4 32) x!189))
; success
(define-fun x!191 () Bool (and x!188 x!190))
; success
(define-fun x!192 () Bool (and (not x!187) (not x!191)))
; success
(assert (not x!192))
; success
(define-fun x!193 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (select x!184 (_ bv5 32)))
; success
(define-fun x!194 () (_ BitVec 32) (struct4-proj1 x!193))
; success
(define-fun x!195 () Bool (= (_ bv0 32) x!194))
; success
(define-fun x!196 () Bool (= (_ bv4 32) x!194))
; success
(define-fun x!197 () (_ BitVec 32) (struct4-proj0 x!193))
; success
(define-fun x!198 () Bool (= (_ bv4 32) x!197))
; success
(define-fun x!199 () Bool (and x!196 x!198))
; success
(define-fun x!200 () Bool (and (not x!195) (not x!199)))
; success
(assert (not x!200))
; success
(define-fun x!201 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (select x!184 (_ bv6 32)))
; success
(define-fun x!202 () (_ BitVec 32) (struct4-proj1 x!201))
; success
(define-fun x!203 () Bool (= (_ bv0 32) x!202))
; success
(define-fun x!204 () Bool (= (_ bv4 32) x!202))
; success
(define-fun x!205 () (_ BitVec 32) (struct4-proj0 x!201))
; success
(define-fun x!206 () Bool (= (_ bv4 32) x!205))
; success
(define-fun x!207 () Bool (and x!204 x!206))
; success
(define-fun x!208 () Bool (and (not x!203) (not x!207)))
; success
(assert (not x!208))
; success
(define-fun x!209 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (select x!184 (_ bv7 32)))
; success
(define-fun x!210 () (_ BitVec 32) (struct4-proj1 x!209))
; success
(define-fun x!211 () Bool (= (_ bv0 32) x!210))
; success
(define-fun x!212 () Bool (= (_ bv4 32) x!210))
; success
(define-fun x!213 () (_ BitVec 32) (struct4-proj0 x!209))
; success
(define-fun x!214 () Bool (= (_ bv4 32) x!213))
; success
(define-fun x!215 () Bool (and x!212 x!214))
; success
(define-fun x!216 () Bool (and (not x!211) (not x!215)))
; success
(assert (not x!216))
; success
(declare-fun x!217 () (_ BitVec 32))
; success
(define-fun x!218 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!217) (_ bv2147483648 32)))
; success
(define-fun x!219 () (_ BitVec 32) (ite x!108 x!218 (_ bv1 32)))
; success
(define-fun x!220 () (_ BitVec 32) (select x!157 x!219))
; success
(define-fun x!221 () Bool (bvult (_ bv4 32) x!220))
; success
(assert x!221)
; success
(define-fun x!222 () Bool (bvult x!220 (_ bv8 32)))
; success
(assert (not x!222))
; success
(pop 1)
; success
(push 1)
; success
(define-fun x!223 () Bool (bvslt x!107 (_ bv0 32)))
; success
(define-fun x!224 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!109) (_ bv2147483648 32)))
; success
(define-fun x!225 () (_ BitVec 32) (ite x!223 x!224 (_ bv1 32)))
; success
(define-fun x!226 () Bool (bvslt x!225 (_ bv0 32)))
; success
(assert x!226)
; success
(pop 1)
; success
(define-fun x!227 () Bool (bvslt x!107 (_ bv0 32)))
; success
(define-fun x!228 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!109) (_ bv2147483648 32)))
; success
(define-fun x!229 () (_ BitVec 32) (ite x!227 x!228 (_ bv1 32)))
; success
(define-fun x!230 () Bool (bvslt x!229 (_ bv0 32)))
; success
(define-fun x!231 () (_ FloatingPoint 8 24) ((_ to_fp 8 24) RNE 0.0))
; success
(define-fun x!232 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (mk-struct4 (_ bv0 32) (_ bv0 32) (_ bv0 32) x!231))
; success
(define-fun x!233 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store x!115 (_ bv0 32) x!232) (_ bv1 32) x!232) (_ bv2 32) x!232) (_ bv3 32) x!232) (_ bv4 32) x!232) (_ bv5 32) x!232) (_ bv6 32) x!232) (_ bv7 32) x!232) (_ bv8 32) x!232) (_ bv9 32) x!232) (_ bv10 32) x!232) (_ bv11 32) x!232) (_ bv12 32) x!232) (_ bv13 32) x!232) (_ bv14 32) x!232) (_ bv15 32) x!232))
; success
(define-fun x!234 () (Array (_ BitVec 32) (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)))) (store x!114 (_ bv1 32) x!233))
; success
(define-fun x!235 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!120) (_ bv2147483648 32)))
; success
(define-fun x!236 () (_ BitVec 32) (ite x!227 x!235 (_ bv1 32)))
; success
(define-fun x!237 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (select x!234 x!236))
; success
(define-fun x!238 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (select x!237 (_ bv0 32)))
; success
(define-fun x!239 () (_ BitVec 32) (struct4-proj1 x!238))
; success
(define-fun x!240 () Bool (= (_ bv0 32) x!239))
; success
(define-fun x!241 () Bool (= (_ bv4 32) x!239))
; success
(define-fun x!242 () (_ BitVec 32) (struct4-proj0 x!238))
; success
(define-fun x!243 () Bool (= (_ bv0 32) x!242))
; success
(define-fun x!244 () Bool (and x!241 x!243))
; success
(define-fun x!245 () Bool (and (not x!240) (not x!244)))
; success
(define-fun x!246 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (select x!237 (_ bv1 32)))
; success
(define-fun x!247 () (_ BitVec 32) (struct4-proj1 x!246))
; success
(define-fun x!248 () Bool (= (_ bv0 32) x!247))
; success
(define-fun x!249 () Bool (= (_ bv4 32) x!247))
; success
(define-fun x!250 () (_ BitVec 32) (struct4-proj0 x!246))
; success
(define-fun x!251 () Bool (= (_ bv0 32) x!250))
; success
(define-fun x!252 () Bool (and x!249 x!251))
; success
(define-fun x!253 () Bool (and (not x!248) (not x!252)))
; success
(define-fun x!254 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (select x!237 (_ bv2 32)))
; success
(define-fun x!255 () (_ BitVec 32) (struct4-proj1 x!254))
; success
(define-fun x!256 () Bool (= (_ bv0 32) x!255))
; success
(define-fun x!257 () Bool (= (_ bv4 32) x!255))
; success
(define-fun x!258 () (_ BitVec 32) (struct4-proj0 x!254))
; success
(define-fun x!259 () Bool (= (_ bv0 32) x!258))
; success
(define-fun x!260 () Bool (and x!257 x!259))
; success
(define-fun x!261 () Bool (and (not x!256) (not x!260)))
; success
(define-fun x!262 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (select x!237 (_ bv3 32)))
; success
(define-fun x!263 () (_ BitVec 32) (struct4-proj1 x!262))
; success
(define-fun x!264 () Bool (= (_ bv0 32) x!263))
; success
(define-fun x!265 () Bool (= (_ bv4 32) x!263))
; success
(define-fun x!266 () (_ BitVec 32) (struct4-proj0 x!262))
; success
(define-fun x!267 () Bool (= (_ bv0 32) x!266))
; success
(define-fun x!268 () Bool (and x!265 x!267))
; success
(define-fun x!269 () Bool (and (not x!264) (not x!268)))
; success
(define-fun x!270 () Bool (and (not x!245) (not x!253) (not x!261) (not x!269)))
; success
(define-fun x!271 () Bool (and (not x!230) (not x!270)))
; success
(define-fun x!272 () Bool (not x!271))
; success
(assert x!272)
; success
(define-fun x!273 () (Array (_ BitVec 32) (_ BitVec 32)) (store (store x!156 (_ bv0 32) (_ bv16 32)) (_ bv1 32) (_ bv16 32)))
; success
(define-fun x!274 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!158) (_ bv2147483648 32)))
; success
(define-fun x!275 () (_ BitVec 32) (ite x!227 x!274 (_ bv1 32)))
; success
(define-fun x!276 () (_ BitVec 32) (select x!273 x!275))
; success
(define-fun x!277 () Bool (bvult (_ bv0 32) x!276))
; success
(define-fun x!278 () Bool (bvult x!276 (_ bv4 32)))
; success
(define-fun x!279 () Bool (and x!277 (not x!278)))
; success
(define-fun x!280 () Bool (and (not x!230) (not x!279)))
; success
(define-fun x!281 () Bool (not x!280))
; success
(assert x!281)
; success
(define-fun x!282 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!164) (_ bv2147483648 32)))
; success
(define-fun x!283 () (_ BitVec 32) (ite x!227 x!282 (_ bv1 32)))
; success
(define-fun x!284 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (select x!234 x!283))
; success
(define-fun x!285 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (mk-struct4 (_ bv0 32) (_ bv4 32) (_ bv5 32) x!168))
; success
(define-fun x!286 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (store x!284 (_ bv0 32) x!285))
; success
(define-fun x!287 () (Array (_ BitVec 32) (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)))) (store x!234 x!283 x!286))
; success
(define-fun x!288 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (select x!287 x!283))
; success
(define-fun x!289 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (store x!288 (_ bv1 32) x!285))
; success
(define-fun x!290 () (Array (_ BitVec 32) (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)))) (store x!287 x!283 x!289))
; success
(define-fun x!291 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (select x!290 x!283))
; success
(define-fun x!292 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (store x!291 (_ bv2 32) x!285))
; success
(define-fun x!293 () (Array (_ BitVec 32) (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)))) (store x!290 x!283 x!292))
; success
(define-fun x!294 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (select x!293 x!283))
; success
(define-fun x!295 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (store x!294 (_ bv3 32) x!285))
; success
(define-fun x!296 () (Array (_ BitVec 32) (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)))) (store x!293 x!283 x!295))
; success
(define-fun x!297 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!181) (_ bv2147483648 32)))
; success
(define-fun x!298 () (_ BitVec 32) (ite x!227 x!297 (_ bv1 32)))
; success
(define-fun x!299 () (Array (_ BitVec 32) (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24))) (select x!296 x!298))
; success
(define-fun x!300 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (select x!299 (_ bv4 32)))
; success
(define-fun x!301 () (_ BitVec 32) (struct4-proj1 x!300))
; success
(define-fun x!302 () Bool (= (_ bv0 32) x!301))
; success
(define-fun x!303 () Bool (= (_ bv4 32) x!301))
; success
(define-fun x!304 () (_ BitVec 32) (struct4-proj0 x!300))
; success
(define-fun x!305 () Bool (= (_ bv4 32) x!304))
; success
(define-fun x!306 () Bool (and x!303 x!305))
; success
(define-fun x!307 () Bool (and (not x!302) (not x!306)))
; success
(define-fun x!308 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (select x!299 (_ bv5 32)))
; success
(define-fun x!309 () (_ BitVec 32) (struct4-proj1 x!308))
; success
(define-fun x!310 () Bool (= (_ bv0 32) x!309))
; success
(define-fun x!311 () Bool (= (_ bv4 32) x!309))
; success
(define-fun x!312 () (_ BitVec 32) (struct4-proj0 x!308))
; success
(define-fun x!313 () Bool (= (_ bv4 32) x!312))
; success
(define-fun x!314 () Bool (and x!311 x!313))
; success
(define-fun x!315 () Bool (and (not x!310) (not x!314)))
; success
(define-fun x!316 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (select x!299 (_ bv6 32)))
; success
(define-fun x!317 () (_ BitVec 32) (struct4-proj1 x!316))
; success
(define-fun x!318 () Bool (= (_ bv0 32) x!317))
; success
(define-fun x!319 () Bool (= (_ bv4 32) x!317))
; success
(define-fun x!320 () (_ BitVec 32) (struct4-proj0 x!316))
; success
(define-fun x!321 () Bool (= (_ bv4 32) x!320))
; success
(define-fun x!322 () Bool (and x!319 x!321))
; success
(define-fun x!323 () Bool (and (not x!318) (not x!322)))
; success
(define-fun x!324 () (Struct4 (_ BitVec 32) (_ BitVec 32) (_ BitVec 32) (_ FloatingPoint 8 24)) (select x!299 (_ bv7 32)))
; success
(define-fun x!325 () (_ BitVec 32) (struct4-proj1 x!324))
; success
(define-fun x!326 () Bool (= (_ bv0 32) x!325))
; success
(define-fun x!327 () Bool (= (_ bv4 32) x!325))
; success
(define-fun x!328 () (_ BitVec 32) (struct4-proj0 x!324))
; success
(define-fun x!329 () Bool (= (_ bv4 32) x!328))
; success
(define-fun x!330 () Bool (and x!327 x!329))
; success
(define-fun x!331 () Bool (and (not x!326) (not x!330)))
; success
(define-fun x!332 () Bool (and (not x!307) (not x!315) (not x!323) (not x!331)))
; success
(define-fun x!333 () Bool (and (not x!230) (not x!332)))
; success
(define-fun x!334 () Bool (not x!333))
; success
(assert x!334)
; success
(define-fun x!335 () (_ BitVec 32) (bvxor (bvand (_ bv2147483647 32) x!217) (_ bv2147483648 32)))
; success
(define-fun x!336 () (_ BitVec 32) (ite x!227 x!335 (_ bv1 32)))
; success
(define-fun x!337 () (_ BitVec 32) (select x!273 x!336))
; success
(define-fun x!338 () Bool (bvult (_ bv4 32) x!337))
; success
(define-fun x!339 () Bool (bvult x!337 (_ bv8 32)))
; success
(define-fun x!340 () Bool (and x!338 (not x!339)))
; success
(define-fun x!341 () Bool (and (not x!230) (not x!340)))
; success
(define-fun x!342 () Bool (not x!341))
; success
(assert x!342)
; success
(declare-fun x!343 () (_ BitVec 32))
; success
(define-fun x!344 () Bool (= (_ bv0 32) x!343))
; success
(declare-fun x!345 () (_ BitVec 32))
; success
(define-fun x!346 () (_ BitVec 32) (bvudiv x!343 (_ bv1 32)))
; success
(define-fun x!347 () Bool (bvult x!345 x!346))
; success
(define-fun x!348 () Bool (and (not x!344) (not x!347)))
; success
(define-fun x!349 () Bool (not x!348))
; success
(assert x!349)
; success
(declare-fun x!350 () (_ BitVec 32))
; success
(define-fun x!351 () Bool (bvult x!350 (_ bv5000000 32)))
; success
(assert x!351)
; success
(declare-fun x!352 () (_ BitVec 32))
; success
(define-fun x!353 () (_ BitVec 32) (bvudiv x!352 (_ bv1000 32)))
; success
(define-fun x!354 () Bool (bvult x!353 x!343))
; success
(define-fun x!355 () Bool (and (not x!344) (not x!354)))
; success
(define-fun x!356 () Bool (not x!355))
; success
(assert x!356)
; success
(push 1)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment