(benchmark ESBMC
:status unknown
:logic QF_AUFLIRA
:datatypes ((pointer_tuple_Int (pointer_tuple_Int (object Int)(index Int)) ))
:datatypes ((struct_type___pthread_internal_slist (struct_type___pthread_internal_slist (__next pointer_tuple_Int)) ))
:datatypes ((struct_type___pthread_mutex_s (struct_type___pthread_mutex_s (__lock Int)(__count Int)(__owner Int)(__kind Int)(__nusers Int)(__list struct_type___pthread_internal_slist)(__spins Int)) ))
:datatypes ((|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| (__data struct_type___pthread_mutex_s)(__size (Array Int Int))(__align Int)(id Int)) ))
:extrafuns ((|c::m&0#8|  |union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']|))
:extrafuns ((|c::m&0#10|  |union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']|))
:extrafuns ((|c::m&0#12|  |union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']|))
:extrafuns ((|#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']|  |union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']|))
:extrafuns ((conv_struct___pthread_mutex_s  struct_type___pthread_mutex_s))
:extrafuns ((|032|  pointer_tuple_Int))
:extrafuns ((|c::m&0#9|  |union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']|))
:extrafuns ((|c::m&0#11|  |union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']|))
:extrafuns ((|c::m&0#13|  |union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']|))
:extrapreds ((l2 ))
:extrapreds ((l1 ))
:extrapreds ((l3 ))
:extrapreds ((l4 ))
:extrapreds ((l5 ))
:extrapreds ((l6 ))
:extrapreds ((l7 ))
:extrapreds ((|execution_statet::\guard_exec@0_0_0&0#1| ))
:extrapreds ((l8 ))
:extrapreds ((l9 ))
:extrapreds ((l10 ))
:extrapreds ((l11 ))
:extrapreds ((l12 ))
:extrapreds ((l13 ))
:extrapreds ((l14 ))
:extrapreds ((l15 ))
:extrapreds ((l16 ))
:extrapreds ((l17 ))
:extrapreds ((l18 ))
:extrapreds ((l19 ))
:extrapreds ((l20 ))
:extrapreds ((l21 ))
:assumption
(let (?x4 (__data |c::m&0#8|))
(let (?x5 (__lock ?x4))
(flet ($x7 (= ?x5 0))
(iff l2 $x7))))
:assumption
(flet ($x29 (and l1 l2))
(iff l3 $x29))
:assumption
(let (?x35 (__data |c::m&0#10|))
(let (?x36 (__lock ?x35))
(flet ($x37 (= ?x36 0))
(iff l4 $x37))))
:assumption
(flet ($x43 (and l1 l2 l4))
(iff l5 $x43))
:assumption
(let (?x49 (__data |c::m&0#12|))
(let (?x50 (__lock ?x49))
(flet ($x51 (= ?x50 0))
(iff l6 $x51))))
:assumption
(flet ($x57 (and l1 l2 l4 l6))
(iff l7 $x57))
:assumption
l1
:assumption
(iff |execution_statet::\guard_exec@0_0_0&0#1| true)
:assumption
(let (?x123 (id |#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']|))
(let (?x122 (__align |#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']|))
(let (?x121 (__size |#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']|))
(let (?x71 (__spins conv_struct___pthread_mutex_s))
(let (?x70 (__list conv_struct___pthread_mutex_s))
(let (?x69 (__nusers conv_struct___pthread_mutex_s))
(let (?x68 (__kind conv_struct___pthread_mutex_s))
(let (?x67 (__owner conv_struct___pthread_mutex_s))
(let (?x66 (__count conv_struct___pthread_mutex_s))
(let (?x72 (struct_type___pthread_mutex_s 0 ?x66 ?x67 ?x68 ?x69 ?x70 ?x71))
(let (?x78 (__spins ?x72))
(let (?x77 (__list ?x72))
(let (?x76 (__nusers ?x72))
(let (?x75 (__kind ?x72))
(let (?x74 (__owner ?x72))
(let (?x73 (__lock ?x72))
(let (?x79 (struct_type___pthread_mutex_s ?x73 0 ?x74 ?x75 ?x76 ?x77 ?x78))
(let (?x85 (__spins ?x79))
(let (?x84 (__list ?x79))
(let (?x83 (__nusers ?x79))
(let (?x82 (__kind ?x79))
(let (?x81 (__count ?x79))
(let (?x80 (__lock ?x79))
(let (?x86 (struct_type___pthread_mutex_s ?x80 ?x81 0 ?x82 ?x83 ?x84 ?x85))
(let (?x92 (__spins ?x86))
(let (?x91 (__list ?x86))
(let (?x90 (__nusers ?x86))
(let (?x89 (__owner ?x86))
(let (?x88 (__count ?x86))
(let (?x87 (__lock ?x86))
(let (?x93 (struct_type___pthread_mutex_s ?x87 ?x88 ?x89 0 ?x90 ?x91 ?x92))
(let (?x99 (__spins ?x93))
(let (?x98 (__list ?x93))
(let (?x97 (__kind ?x93))
(let (?x96 (__owner ?x93))
(let (?x95 (__count ?x93))
(let (?x94 (__lock ?x93))
(let (?x100 (struct_type___pthread_mutex_s ?x94 ?x95 ?x96 ?x97 0 ?x98 ?x99))
(let (?x112 (__spins ?x100))
(let (?x104 (object |032|))
(let (?x105 (pointer_tuple_Int ?x104 (~ 1)))
(let (?x106 (struct_type___pthread_internal_slist ?x105))
(let (?x111 (__nusers ?x100))
(let (?x110 (__kind ?x100))
(let (?x109 (__owner ?x100))
(let (?x108 (__count ?x100))
(let (?x107 (__lock ?x100))
(let (?x113 (struct_type___pthread_mutex_s ?x107 ?x108 ?x109 ?x110 ?x111 ?x106 ?x112))
(let (?x119 (__list ?x113))
(let (?x118 (__nusers ?x113))
(let (?x117 (__kind ?x113))
(let (?x116 (__owner ?x113))
(let (?x115 (__count ?x113))
(let (?x114 (__lock ?x113))
(let (?x120 (struct_type___pthread_mutex_s ?x114 ?x115 ?x116 ?x117 ?x118 ?x119 0))
(let (?x124 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x120 ?x121 ?x122 ?x123))
(let (?x127 (__align ?x124))
(let (?x126 (__size ?x124))
(let (?x125 (__data ?x124))
(let (?x128 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x125 ?x126 ?x127 0))
(let (?x139 (id ?x128))
(let (?x138 (__align ?x128))
(let (?x137 (__size ?x128))
(let (?x129 (__data ?x128))
(let (?x135 (__spins ?x129))
(let (?x134 (__list ?x129))
(let (?x133 (__nusers ?x129))
(let (?x132 (__kind ?x129))
(let (?x131 (__owner ?x129))
(let (?x130 (__count ?x129))
(let (?x136 (struct_type___pthread_mutex_s 0 ?x130 ?x131 ?x132 ?x133 ?x134 ?x135))
(let (?x140 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x136 ?x137 ?x138 ?x139))
(let (?x143 (__align ?x140))
(let (?x142 (__size ?x140))
(let (?x141 (__data ?x140))
(let (?x144 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x141 ?x142 ?x143 0))
(let (?x154 (id ?x144))
(let (?x153 (__align ?x144))
(let (?x152 (__size ?x144))
(let (?x150 (__spins ?x136))
(let (?x149 (__list ?x136))
(let (?x148 (__nusers ?x136))
(let (?x147 (__kind ?x136))
(let (?x146 (__owner ?x136))
(let (?x145 (__lock ?x136))
(let (?x151 (struct_type___pthread_mutex_s ?x145 0 ?x146 ?x147 ?x148 ?x149 ?x150))
(let (?x155 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x151 ?x152 ?x153 ?x154))
(let (?x158 (__align ?x155))
(let (?x157 (__size ?x155))
(let (?x156 (__data ?x155))
(let (?x159 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x156 ?x157 ?x158 0))
(let (?x169 (id ?x159))
(let (?x168 (__align ?x159))
(let (?x167 (__size ?x159))
(let (?x165 (__spins ?x151))
(let (?x164 (__list ?x151))
(let (?x163 (__nusers ?x151))
(let (?x162 (__kind ?x151))
(let (?x161 (__count ?x151))
(let (?x160 (__lock ?x151))
(let (?x166 (struct_type___pthread_mutex_s ?x160 ?x161 0 ?x162 ?x163 ?x164 ?x165))
(let (?x170 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x166 ?x167 ?x168 ?x169))
(let (?x173 (__align ?x170))
(let (?x172 (__size ?x170))
(let (?x171 (__data ?x170))
(let (?x174 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x171 ?x172 ?x173 0))
(let (?x185 (id ?x174))
(let (?x184 (__align ?x174))
(let (?x183 (__size ?x174))
(let (?x181 (__spins ?x166))
(let (?x180 (__list ?x166))
(let (?x179 (__nusers ?x166))
(let (?x178 (__kind ?x166))
(let (?x177 (__owner ?x166))
(let (?x176 (__count ?x166))
(let (?x182 (struct_type___pthread_mutex_s 1 ?x176 ?x177 ?x178 ?x179 ?x180 ?x181))
(let (?x186 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x182 ?x183 ?x184 ?x185))
(let (?x189 (__align ?x186))
(let (?x188 (__size ?x186))
(let (?x187 (__data ?x186))
(let (?x190 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x187 ?x188 ?x189 0))
(let (?x200 (id ?x190))
(let (?x199 (__align ?x190))
(let (?x198 (__size ?x190))
(let (?x196 (__spins ?x182))
(let (?x195 (__list ?x182))
(let (?x194 (__nusers ?x182))
(let (?x193 (__kind ?x182))
(let (?x192 (__owner ?x182))
(let (?x191 (__count ?x182))
(let (?x197 (struct_type___pthread_mutex_s 0 ?x191 ?x192 ?x193 ?x194 ?x195 ?x196))
(let (?x201 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x197 ?x198 ?x199 ?x200))
(let (?x204 (__align ?x201))
(let (?x203 (__size ?x201))
(let (?x202 (__data ?x201))
(let (?x205 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x202 ?x203 ?x204 0))
(let (?x215 (id ?x205))
(let (?x214 (__align ?x205))
(let (?x213 (__size ?x205))
(let (?x211 (__spins ?x197))
(let (?x210 (__list ?x197))
(let (?x209 (__nusers ?x197))
(let (?x208 (__kind ?x197))
(let (?x207 (__owner ?x197))
(let (?x206 (__count ?x197))
(let (?x212 (struct_type___pthread_mutex_s 1 ?x206 ?x207 ?x208 ?x209 ?x210 ?x211))
(let (?x216 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x212 ?x213 ?x214 ?x215))
(let (?x219 (__align ?x216))
(let (?x218 (__size ?x216))
(let (?x217 (__data ?x216))
(let (?x220 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x217 ?x218 ?x219 0))
(let (?x230 (id ?x220))
(let (?x229 (__align ?x220))
(let (?x228 (__size ?x220))
(let (?x226 (__spins ?x212))
(let (?x225 (__list ?x212))
(let (?x224 (__nusers ?x212))
(let (?x223 (__kind ?x212))
(let (?x222 (__owner ?x212))
(let (?x221 (__count ?x212))
(let (?x227 (struct_type___pthread_mutex_s 0 ?x221 ?x222 ?x223 ?x224 ?x225 ?x226))
(let (?x231 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x227 ?x228 ?x229 ?x230))
(let (?x234 (__align ?x231))
(let (?x233 (__size ?x231))
(let (?x232 (__data ?x231))
(let (?x235 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x232 ?x233 ?x234 0))
(= |c::m&0#8| ?x235)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
:assumption
(let (?x258 (id |c::m&0#8|))
(let (?x257 (__align |c::m&0#8|))
(let (?x256 (__size |c::m&0#8|))
(let (?x4 (__data |c::m&0#8|))
(let (?x254 (__spins ?x4))
(let (?x253 (__list ?x4))
(let (?x252 (__nusers ?x4))
(let (?x251 (__kind ?x4))
(let (?x250 (__owner ?x4))
(let (?x249 (__count ?x4))
(let (?x255 (struct_type___pthread_mutex_s 1 ?x249 ?x250 ?x251 ?x252 ?x253 ?x254))
(let (?x259 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x255 ?x256 ?x257 ?x258))
(let (?x262 (__align ?x259))
(let (?x261 (__size ?x259))
(let (?x260 (__data ?x259))
(let (?x263 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x260 ?x261 ?x262 0))
(= |c::m&0#9| ?x263)))))))))))))))))
:assumption
(let (?x277 (id |c::m&0#9|))
(let (?x276 (__align |c::m&0#9|))
(let (?x275 (__size |c::m&0#9|))
(let (?x267 (__data |c::m&0#9|))
(let (?x273 (__spins ?x267))
(let (?x272 (__list ?x267))
(let (?x271 (__nusers ?x267))
(let (?x270 (__kind ?x267))
(let (?x269 (__owner ?x267))
(let (?x268 (__count ?x267))
(let (?x274 (struct_type___pthread_mutex_s 0 ?x268 ?x269 ?x270 ?x271 ?x272 ?x273))
(let (?x278 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x274 ?x275 ?x276 ?x277))
(let (?x281 (__align ?x278))
(let (?x280 (__size ?x278))
(let (?x279 (__data ?x278))
(let (?x282 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x279 ?x280 ?x281 0))
(= |c::m&0#10| ?x282)))))))))))))))))
:assumption
(let (?x296 (id |c::m&0#10|))
(let (?x295 (__align |c::m&0#10|))
(let (?x294 (__size |c::m&0#10|))
(let (?x35 (__data |c::m&0#10|))
(let (?x292 (__spins ?x35))
(let (?x291 (__list ?x35))
(let (?x290 (__nusers ?x35))
(let (?x289 (__kind ?x35))
(let (?x288 (__owner ?x35))
(let (?x287 (__count ?x35))
(let (?x293 (struct_type___pthread_mutex_s 1 ?x287 ?x288 ?x289 ?x290 ?x291 ?x292))
(let (?x297 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x293 ?x294 ?x295 ?x296))
(let (?x300 (__align ?x297))
(let (?x299 (__size ?x297))
(let (?x298 (__data ?x297))
(let (?x301 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x298 ?x299 ?x300 0))
(= |c::m&0#11| ?x301)))))))))))))))))
:assumption
(let (?x315 (id |c::m&0#11|))
(let (?x314 (__align |c::m&0#11|))
(let (?x313 (__size |c::m&0#11|))
(let (?x305 (__data |c::m&0#11|))
(let (?x311 (__spins ?x305))
(let (?x310 (__list ?x305))
(let (?x309 (__nusers ?x305))
(let (?x308 (__kind ?x305))
(let (?x307 (__owner ?x305))
(let (?x306 (__count ?x305))
(let (?x312 (struct_type___pthread_mutex_s 0 ?x306 ?x307 ?x308 ?x309 ?x310 ?x311))
(let (?x316 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x312 ?x313 ?x314 ?x315))
(let (?x319 (__align ?x316))
(let (?x318 (__size ?x316))
(let (?x317 (__data ?x316))
(let (?x320 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x317 ?x318 ?x319 0))
(= |c::m&0#12| ?x320)))))))))))))))))
:assumption
(let (?x334 (id |c::m&0#12|))
(let (?x333 (__align |c::m&0#12|))
(let (?x332 (__size |c::m&0#12|))
(let (?x49 (__data |c::m&0#12|))
(let (?x330 (__spins ?x49))
(let (?x329 (__list ?x49))
(let (?x328 (__nusers ?x49))
(let (?x327 (__kind ?x49))
(let (?x326 (__owner ?x49))
(let (?x325 (__count ?x49))
(let (?x331 (struct_type___pthread_mutex_s 1 ?x325 ?x326 ?x327 ?x328 ?x329 ?x330))
(let (?x335 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x331 ?x332 ?x333 ?x334))
(let (?x338 (__align ?x335))
(let (?x337 (__size ?x335))
(let (?x336 (__data ?x335))
(let (?x339 (|union_type_#anon#UN[SYM#c::tag-__pthread_mutex_s#'__data'\|ARR00000000000000000000000000011000{S8}'__size'\|S32'__align']| ?x336 ?x337 ?x338 0))
(= |c::m&0#13| ?x339)))))))))))))))))
:assumption
(flet ($x343 (not l1))
(flet ($x344 (or $x343 l2))
(iff l8 $x344)))
:assumption
(flet ($x349 (not l3))
(flet ($x350 (or $x349 l4))
(iff l9 $x350)))
:assumption
(flet ($x354 (not l5))
(flet ($x355 (or $x354 l6))
(iff l10 $x355)))
:assumption
(let (?x267 (__data |c::m&0#9|))
(let (?x359 (__lock ?x267))
(flet ($x360 (= ?x359 0))
(iff l11 $x360))))
:assumption
(flet ($x366 (not l11))
(flet ($x349 (not l3))
(flet ($x367 (or $x349 $x366))
(iff l12 $x367))))
:assumption
(flet ($x371 (not l8))
(flet ($x372 (or $x371 l12))
(iff l13 $x372)))
:assumption
(flet ($x376 (and l8 l9))
(iff l14 $x376))
:assumption
(let (?x305 (__data |c::m&0#11|))
(let (?x380 (__lock ?x305))
(flet ($x381 (= ?x380 0))
(iff l15 $x381))))
:assumption
(flet ($x387 (not l15))
(flet ($x354 (not l5))
(flet ($x388 (or $x354 $x387))
(iff l16 $x388))))
:assumption
(flet ($x392 (not l14))
(flet ($x393 (or $x392 l16))
(iff l17 $x393)))
:assumption
(flet ($x397 (and l14 l10))
(iff l18 $x397))
:assumption
(let (?x402 (__data |c::m&0#13|))
(let (?x403 (__lock ?x402))
(flet ($x404 (= ?x403 0))
(iff l19 $x404))))
:assumption
(flet ($x411 (not l19))
(flet ($x410 (not l7))
(flet ($x412 (or $x410 $x411))
(iff l20 $x412))))
:assumption
(flet ($x416 (not l18))
(flet ($x417 (or $x416 l20))
(iff l21 $x417)))
:assumption
(flet ($x423 (not l21))
(flet ($x422 (not l17))
(flet ($x421 (not l13))
(or $x421 $x422 $x423))))
:formula
true
)

