; benchmark
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-sort Term)
(declare-fun C72 () Term)
(declare-fun ip () Term)
(declare-fun main_$p0 () (_ BitVec 32))
(declare-fun $M.2.i32 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun main_$p0+ () (_ BitVec 32))
(declare-fun C19 () Term)
(declare-fun C68 () Term)
(declare-fun $alloca_retloc () Term)
(declare-fun $alloca_$r () (_ BitVec 32))
(declare-fun $M.2.i32+ () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun C84 () Term)
(declare-fun getchar_0 () (_ BitVec 32))
(declare-fun main_$p2 () (_ BitVec 32))
(declare-fun C118 () Term)
(declare-fun ip+ () Term)
(declare-fun C116 () Term)
(declare-fun C115 () Term)
(declare-fun C102 () Term)
(declare-fun C100 () Term)
(declare-fun C92 () Term)
(declare-fun C76 () Term)
(declare-fun C70 () Term)
(declare-fun C69 () Term)
(declare-fun C15 () Term)
(declare-fun C67 () Term)
(declare-fun C27 () Term)
(declare-fun C25 () Term)
(declare-fun C66 () Term)
(declare-fun C14 () Term)
(declare-fun C11 () Term)
(declare-fun C65 () Term)
(declare-fun C1 () Term)
(declare-fun C17 () Term)
(declare-fun $init_funcs_retloc () Term)
(declare-fun $static_init_retloc () Term)
(declare-fun C13 () Term)
(declare-fun $5.ref () (_ BitVec 32))
(declare-fun $5.ref+ () (_ BitVec 32))
(declare-fun $3.ref () (_ BitVec 32))
(declare-fun $3.ref+ () (_ BitVec 32))
(declare-fun $4.ref () (_ BitVec 32))
(declare-fun $4.ref+ () (_ BitVec 32))
(declare-fun $0.ref () (_ BitVec 32))
(declare-fun $0.ref+ () (_ BitVec 32))
(declare-fun $1.ref () (_ BitVec 32))
(declare-fun $1.ref+ () (_ BitVec 32))
(declare-fun $2.ref () (_ BitVec 32))
(declare-fun $2.ref+ () (_ BitVec 32))
(declare-fun $GLOBALS_BOTTOM () (_ BitVec 32))
(declare-fun $GLOBALS_BOTTOM+ () (_ BitVec 32))
(declare-fun $EXTERNS_BOTTOM () (_ BitVec 32))
(declare-fun $EXTERNS_BOTTOM+ () (_ BitVec 32))
(declare-fun $MALLOC_TOP () (_ BitVec 32))
(declare-fun $MALLOC_TOP+ () (_ BitVec 32))
(declare-fun $7.ref () (_ BitVec 32))
(declare-fun $7.ref+ () (_ BitVec 32))
(declare-fun $6.ref () (_ BitVec 32))
(declare-fun $6.ref+ () (_ BitVec 32))
(declare-fun main_$p12 () Bool)
(declare-fun main_$p12+ () Bool)
(declare-fun main_$p3 () Bool)
(declare-fun b!726 () Bool)
(declare-fun b!391 () Bool)
(declare-fun b!285 () Bool)
(declare-fun b!36 () Bool)
(declare-fun b!31 () Bool)
(declare-fun b!30 () Bool)
(declare-fun b!29 () Bool)
(declare-fun b!28 () Bool)
(declare-fun b!27 () Bool)
(declare-fun b!26 () Bool)
(declare-fun b!25 () Bool)
(declare-fun b!24 () Bool)
(declare-fun b!23 () Bool)
(declare-fun b!22 () Bool)
(declare-fun b!21 () Bool)
(declare-fun b!287 () Bool)
(declare-fun b!440 () Bool)
(declare-fun b!148 () Bool)
(declare-fun b!38 () Bool)
(declare-fun b!613 () Bool)
(declare-fun b!516 () Bool)
(declare-fun b!517 () Bool)
(declare-fun b!245 () Bool)
(declare-fun b!518 () Bool)
(assert
(let (($x380 (= ip C72)))
(let (($x646 (not $x380)))
(let (($x657 (=> $x646 (= main_$p12+ main_$p12))))
(let (($x415 (and $x380 main_$p3)))
(let (($x659 (=> $x415 (= main_$p12+ main_$p12))))
(let ((?x400 (bvadd (_ bv4 32) main_$p0)))
(let ((?x401 (select $M.2.i32 ?x400)))
(let ((?x399 (select $M.2.i32 main_$p0)))
(let (($x402 (bvsle ?x399 ?x401)))
(let (($x403 (not $x402)))
(let (($x389 (not main_$p3)))
(let (($x398 (and $x380 $x389)))
(let (($x405 (=> $x398 (= main_$p12+ $x403))))
(let (($x3556 (and $x405 $x659 $x657)))
(let (($x3783 (=> b!726 $x3556)))
(let (($x728 (= main_$p0+ main_$p0)))
(let (($x306 (= ip C19)))
(let (($x730 (not $x306)))
(let (($x731 (=> $x730 $x728)))
(let (($x729 (=> (and $x306 (not (= $alloca_retloc C68))) $x728)))
(let (($x313 (= main_$p0+ $alloca_$r)))
(let (($x314 (=> (and $x306 (= $alloca_retloc C68)) $x313)))
(let (($x3159 (and $x314 $x729 $x731)))
(let (($x4099 (=> b!391 $x3159)))
(let (($x700 (= $M.2.i32+ $M.2.i32)))
(let (($x704 (=> (and $x646 (not (= ip C84))) $x700)))
(let (($x467 (not main_$p12)))
(let (($x397 (= ip C84)))
(let (($x468 (and $x397 $x467)))
(let (($x702 (=> $x468 $x700)))
(let (($x701 (=> $x398 $x700)))
(let ((?x451 (store $M.2.i32 main_$p0 ?x401)))
(let ((?x452 (store ?x451 ?x400 ?x399)))
(let (($x453 (= $M.2.i32+ ?x452)))
(let (($x450 (and $x397 main_$p12)))
(let (($x454 (=> $x450 $x453)))
(let ((?x419 (bvmul (_ bv4 32) main_$p2)))
(let ((?x423 (bvadd main_$p0 ?x419)))
(let ((?x430 (store $M.2.i32 ?x423 getchar_0)))
(let (($x431 (= $M.2.i32+ ?x430)))
(let (($x432 (=> $x415 $x431)))
(let (($x3313 (and $x432 $x454 $x701 $x702 $x704)))
(let (($x3220 (=> b!285 $x3313)))
(let (($x480 (= ip+ C118)))
(let (($x523 (= ip C118)))
(let (($x526 (=> $x523 $x480)))
(let (($x446 (= ip C116)))
(let (($x525 (or (and (distinct ip+ C118) true) $x446 $x523)))
(let (($x522 (=> $x446 $x480)))
(let (($x516 (= ip C115)))
(let (($x448 (or (and (distinct ip+ C116) true) $x516)))
(let (($x391 (= ip+ C116)))
(let (($x445 (=> $x516 $x391)))
(let (($x510 (= ip C102)))
(let (($x518 (or (and (distinct ip+ C115) true) $x510)))
(let (($x514 (= ip+ C115)))
(let (($x515 (=> $x510 $x514)))
(let (($x414 (= ip C100)))
(let (($x512 (or (and (distinct ip+ C102) true) $x414)))
(let (($x481 (= ip+ C102)))
(let (($x509 (=> $x414 $x481)))
(let (($x472 (= ip C92)))
(let (($x476 (or (and (distinct ip+ C100) true) $x472 $x397)))
(let (($x387 (= ip+ C100)))
(let (($x395 (=> $x472 $x387)))
(let (($x474 (or (and (distinct ip+ C92) true) $x397)))
(let (($x470 (= ip+ C92)))
(let (($x471 (=> $x450 $x470)))
(let (($x469 (=> $x468 $x387)))
(let (($x392 (or (and (distinct ip+ C84) true) $x380)))
(let (($x374 (= ip+ C72)))
(let (($x383 (= ip C76)))
(let (($x396 (=> $x383 $x374)))
(let (($x440 (or (and (distinct ip+ C76) true) $x380)))
(let (($x437 (= ip+ C76)))
(let (($x438 (=> $x415 $x437)))
(let (($x390 (= ip+ C84)))
(let (($x436 (=> $x398 $x390)))
(let (($x369 (= ip C70)))
(let (($x384 (or (and (distinct ip+ C72) true) $x369 $x383)))
(let (($x379 (=> $x369 $x374)))
(let (($x361 (= ip C69)))
(let (($x371 (or (and (distinct ip+ C70) true) $x361)))
(let (($x365 (= ip+ C70)))
(let (($x368 (=> $x361 $x365)))
(let (($x363 (or (and (distinct ip+ C69) true) $x306)))
(let (($x349 (= ip+ C15)))
(let (($x290 (= ip C68)))
(let (($x357 (=> $x290 $x349)))
(let (($x356 (or (and (distinct ip+ C68) true) $x306)))
(let (($x288 (= ip C67)))
(let (($x354 (=> $x288 $x349)))
(let (($x272 (= ip C27)))
(let (($x347 (or (and (distinct ip+ C67) true) $x272)))
(let (($x344 (= ip+ C25)))
(let (($x267 (= ip C66)))
(let (($x345 (=> $x267 $x344)))
(let (($x251 (= ip C14)))
(let (($x341 (or (and (distinct ip+ C66) true) $x251)))
(let (($x338 (= ip+ C11)))
(let (($x237 (= ip C65)))
(let (($x339 (=> $x237 $x338)))
(let (($x329 (= ip C1)))
(let (($x335 (or (and (distinct ip+ C65) true) $x329)))
(let (($x332 (= ip+ C65)))
(let (($x333 (=> $x329 $x332)))
(let (($x331 (or (and (distinct ip+ C1) true))))
(let (($x304 (= ip+ C19)))
(let (($x316 (= $alloca_retloc C69)))
(let (($x325 (not $x316)))
(let (($x311 (= $alloca_retloc C68)))
(let (($x324 (not $x311)))
(let (($x327 (=> (and $x306 $x324 $x325) $x304)))
(let (($x322 (= ip+ C69)))
(let (($x323 (=> (and $x306 $x316) $x322)))
(let (($x320 (= ip+ C68)))
(let (($x321 (=> (and $x306 $x311) $x320)))
(let (($x300 (= ip C17)))
(let (($x308 (or (and (distinct ip+ C19) true) $x300)))
(let (($x305 (=> $x300 $x304)))
(let (($x286 (= ip C15)))
(let (($x302 (or (and (distinct ip+ C17) true) $x286)))
(let (($x294 (= ip+ C17)))
(let (($x299 (=> $x286 $x294)))
(let (($x291 (or (and (distinct ip+ C15) true) $x288 $x290)))
(let (($x270 (= ip+ C27)))
(let (($x284 (=> (and $x272 (not (= $init_funcs_retloc C67))) $x270)))
(let (($x280 (= ip+ C67)))
(let (($x281 (=> (and $x272 (= $init_funcs_retloc C67)) $x280)))
(let (($x265 (= ip C25)))
(let (($x274 (or (and (distinct ip+ C27) true) $x265)))
(let (($x271 (=> $x265 $x270)))
(let (($x268 (or (and (distinct ip+ C25) true) $x267)))
(let (($x249 (= ip+ C14)))
(let (($x263 (=> (and $x251 (not (= $static_init_retloc C66))) $x249)))
(let (($x259 (= ip+ C66)))
(let (($x260 (=> (and $x251 (= $static_init_retloc C66)) $x259)))
(let (($x245 (= ip C13)))
(let (($x253 (or (and (distinct ip+ C14) true) $x245)))
(let (($x250 (=> $x245 $x249)))
(let (($x234 (= ip C11)))
(let (($x247 (or (and (distinct ip+ C13) true) $x234)))
(let (($x241 (= ip+ C13)))
(let (($x244 (=> $x234 $x241)))
(let (($x238 (or (and (distinct ip+ C11) true) $x237)))
(let (($x1880 (and $x238 $x244 $x247 $x250 $x253 $x260 $x263 $x268 $x271 $x274 $x281 $x284 $x291 $x299 $x302 $x305 $x308 $x321 $x323 $x327 $x331 $x333 $x335 $x339 $x341 $x345 $x347 $x354 $x356 $x357 $x363 $x368 $x371 $x379 $x384 $x436 $x438 $x440 $x396 $x392 $x469 $x471 $x474 $x395 $x476 $x509 $x512 $x515 $x518 $x445 $x448 $x522 $x525 $x526)))
(let (($x3247 (=> b!36 $x1880)))
(let (($x546 (=> true (= $5.ref+ $5.ref))))
(let (($x1393 (=> (and b!31 true) (= $5.ref+ $5.ref))))
(let (($x613 (=> true (= $3.ref+ $3.ref))))
(let (($x2155 (=> (and b!30 true) (= $3.ref+ $3.ref))))
(let (($x709 (=> true (= $4.ref+ $4.ref))))
(let (($x1309 (=> (and b!29 true) (= $4.ref+ $4.ref))))
(let (($x766 (=> true (= $0.ref+ $0.ref))))
(let (($x1225 (=> (and b!28 true) (= $0.ref+ $0.ref))))
(let (($x762 (=> true (= $1.ref+ $1.ref))))
(let (($x2258 (=> (and b!27 true) (= $1.ref+ $1.ref))))
(let (($x755 (=> true (= $2.ref+ $2.ref))))
(let (($x1419 (=> (and b!26 true) (= $2.ref+ $2.ref))))
(let (($x726 (=> true (= $GLOBALS_BOTTOM+ $GLOBALS_BOTTOM))))
(let (($x1154 (=> (and b!25 true) (= $GLOBALS_BOTTOM+ $GLOBALS_BOTTOM))))
(let (($x532 (=> true (= $EXTERNS_BOTTOM+ $EXTERNS_BOTTOM))))
(let (($x1455 (=> (and b!24 true) (= $EXTERNS_BOTTOM+ $EXTERNS_BOTTOM))))
(let (($x621 (=> true (= $MALLOC_TOP+ $MALLOC_TOP))))
(let (($x1329 (=> (and b!23 true) (= $MALLOC_TOP+ $MALLOC_TOP))))
(let (($x607 (=> true (= $7.ref+ $7.ref))))
(let (($x1231 (=> (and b!22 true) (= $7.ref+ $7.ref))))
(let (($x615 (=> true (= $6.ref+ $6.ref))))
(let (($x1928 (=> (and b!21 true) (= $6.ref+ $6.ref))))
(let (($x579 (not $x414)))
(let (($x1108 (=> b!287 $x579)))
(let (($x2570 (not $x472)))
(let (($x1806 (=> b!440 $x2570)))
(let (($x2577 (not $x510)))
(let (($x1237 (=> b!148 $x2577)))
(let (($x555 (not $x516)))
(let (($x1646 (=> b!38 $x555)))
(let (($x661 (not $x397)))
(let (($x1935 (=> b!613 $x661)))
(let (($x2091 (not main_$p12+)))
(let (($x1961 (=> b!516 $x2091)))
(let (($x1675 (=> b!517 $x390)))
(let ((?x1121 (bvadd (_ bv4 32) main_$p0+)))
(let ((?x1657 (select $M.2.i32+ ?x1121)))
(let ((?x1224 (select $M.2.i32+ main_$p0+)))
(let (($x1655 (bvsle ?x1224 ?x1657)))
(let (($x1622 (not $x1655)))
(let (($x965 (=> b!245 $x1622)))
(let (($x1668 (or $x402 main_$p12 $x661)))
(let (($x1043 (=> b!518 $x1668)))
(let (($x775 (= ip+ C1)))
(let (($x776 (or $x320 $x344 $x304 $x241 $x480 $x294 $x349 $x259 $x322 $x775 $x280 $x332 $x338 $x374 $x390 $x470 $x270 $x249 $x387 $x365 $x481 $x514 $x391 $x437)))
(let (($x774 (or $x290 $x265 $x306 $x245 $x523 $x300 $x286 $x267 $x361 $x329 $x288 $x237 $x234 $x380 $x397 $x472 $x272 $x251 $x414 $x369 $x510 $x516 $x446 $x383)))
(let (($x773 (and (distinct C68 C25 C19 C13 C118 C17 C15 C66 C69 C1 C67 C65 C11 C72 C84 C92 C27 C14 C100 C70 C102 C115 C116 C76) true)))
(let (($x777 (and (= $0.ref (_ bv0 32)) (= $GLOBALS_BOTTOM (_ bv4294967276 32)) (= $EXTERNS_BOTTOM (_ bv4294934528 32)) (= $MALLOC_TOP (_ bv2136997887 32)) (= $1.ref (_ bv1 32)) (= $2.ref (_ bv2 32)) (= $3.ref (_ bv3 32)) (= $4.ref (_ bv4 32)) (= $5.ref (_ bv5 32)) (= $6.ref (_ bv6 32)) (= $7.ref (_ bv7 32)) $x773 $x774 $x776)))
(and $x777 $x1043 $x965 $x1675 $x1961 $x1935 $x1646 $x1237 $x1806 $x1108 $x1928 $x1231 $x1329 $x1455 $x1154 $x1419 $x2258 $x1225 $x1309 $x2155 $x1393 $x3247 $x3220 $x4099 $x3783 b!518 b!245 b!517 b!516 b!613 b!38 b!148 b!440 b!287 b!21 b!22 b!23 b!24 b!25 b!26 b!27 b!28 b!29 b!30 b!31 b!36 b!285 b!391
;; comment out the following line and the problem is immediately sat
b!726
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)