(set-logic QF_ABV)
(set-info :status unknown)
(set-info :category "industrial")
(set-info :source "Generated using the Low-Level Bounded Model Checker LLBMC")
(define-fun v1 () (_ BitVec 32) (_ bv0 32))
(define-fun v2 () (_ BitVec 32) (_ bv1 32))
(define-fun v3 () (_ BitVec 32) (_ bv2 32))
(define-fun v4 () (_ BitVec 32) (_ bv3 32))
(define-fun v5 () (_ BitVec 32) (_ bv4 32))
(define-fun v6 () (_ BitVec 32) (_ bv100000 32))
(define-fun v7 () (_ BitVec 32) (_ bv542113792 32))
(define-fun v8 () (_ BitVec 32) (_ bv1605369856 32))
(define-fun v9 () (_ BitVec 32) (_ bv4294967295 32))
(define-fun v10 () (_ BitVec 32) (_ bv542113792 32))
(define-fun v11 () (_ BitVec 32) (_ bv542113792 32))
(declare-fun initialMemoryState_0x8c7e090 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun n_0x8c82ea8 () (_ BitVec 32))
(define-fun b12 () Bool (bvsgt n_0x8c82ea8 v1))
(define-fun b13 () Bool (bvslt n_0x8c82ea8 v6))
(define-fun b14 () Bool (and b12 b13))
(define-fun v15 () (_ BitVec 32) (bvmul n_0x8c82ea8 v5))
(define-fun b16 () Bool (bvule v15 v8))
(define-fun b17 () Bool (and b14 b16))
(define-fun b18 () Bool (bvslt v1 n_0x8c82ea8))
(define-fun b19 () Bool (and b17 b18))
(define-fun v20 () (_ BitVec 32) (bvadd v9 n_0x8c82ea8))
(define-fun v21 () (_ BitVec 32) (bvadd v20 v2))
(define-fun v22 () (_ BitVec 32) (bvmul v21 v5))
(define-fun v23 () (_ BitVec 32) (bvadd v7 v22))
(define-fun a24 ((i (_ BitVec 32))) (_ BitVec 8)
(let ((?x1 (select initialMemoryState_0x8c7e090 i)))
(let ((?x2 (bvsub i v7)))
(let ((?x3 ((_ extract 4 0) v3)))
(let ((?x4 ((_ zero_extend 27) ?x3)))
(let ((?x5 (bvlshr ?x2 ?x4)))
(let ((?x6 (_ bv4 32)))
(let ((?x7 (bvmul ?x6 ?x5)))
(let ((?x8 (bvadd v11 ?x7)))
(let ((?x9 (_ bv1 32)))
(let ((?x10 (select initialMemoryState_0x8c7e090 ?x8)))
(let ((?x11 (bvadd ?x8 ?x9)))
(let ((?x12 (select initialMemoryState_0x8c7e090 ?x11)))
(let ((?x13 (bvadd ?x11 ?x9)))
(let ((?x14 (select initialMemoryState_0x8c7e090 ?x13)))
(let ((?x15 (bvadd ?x13 ?x9)))
(let ((?x16 (select initialMemoryState_0x8c7e090 ?x15)))
(let ((?x17 (concat ?x12 ?x10)))
(let ((?x18 (concat ?x14 ?x17)))
(let ((?x19 (concat ?x16 ?x18)))
(let ((?x20 (bvmul v3 ?x19)))
(let ((?x21 (bvadd ?x20 v2)))
(let ((?x22 ((_ extract 31 24) ?x21)))
(let ((?x23 ((_ extract 23 16) ?x21)))
(let ((?x24 (bvand ?x2 v4)))
(let (($x25 (= ?x24 v3)))
(let ((?x26 (ite $x25 ?x23 ?x22)))
(let ((?x27 ((_ extract 15 8) ?x21)))
(let (($x28 (= ?x24 v2)))
(let ((?x29 (ite $x28 ?x27 ?x26)))
(let ((?x30 ((_ extract 7 0) ?x21)))
(let (($x31 (= ?x24 v1)))
(let ((?x32 (ite $x31 ?x30 ?x29)))
(let (($x33 (bvult i v23)))
(let (($x34 (bvule v10 i)))
(let (($x35 (and $x34 $x33)))
(let ((?x36 (ite $x35 ?x32 ?x1)))
?x36
))))))))))))))))))))))))))))))))))))
)
(define-fun a25 () (Array (_ BitVec 32) (_ BitVec 8)) (ite b19 a24 initialMemoryState_0x8c7e090))
(define-fun v26 () (_ BitVec 32) (_ bv542113792 32))
(define-fun v27 () (_ BitVec 8) (select a25 v26))
(define-fun v28 () (_ BitVec 32) (_ bv542113793 32))
(define-fun v29 () (_ BitVec 8) (select a25 v28))
(define-fun v30 () (_ BitVec 32) (_ bv542113794 32))
(define-fun v31 () (_ BitVec 8) (select a25 v30))
(define-fun v32 () (_ BitVec 32) (_ bv542113795 32))
(define-fun v33 () (_ BitVec 8) (select a25 v32))
(define-fun v34 () (_ BitVec 16) (concat v29 v27))
(define-fun v35 () (_ BitVec 24) (concat v31 v34))
(define-fun v36 () (_ BitVec 32) (concat v33 v35))
(define-fun b37 () Bool (= v36 v2))
(define-fun b38 () Bool (not b17))
(define-fun b39 () Bool (or b38 b37))
(define-fun b40 () Bool (not b39))
(assert b40)
(check-sat)
(exit)