(set-logic QF_ABV)
(set-info :status sat)
(declare-const a0 (Array (_ BitVec 4) (_ BitVec 4) ))
(declare-const v0 (_ BitVec 2))
(declare-const a1 (Array (_ BitVec 3) (_ BitVec 1) ))
(declare-const v1 (_ BitVec 3))
(declare-const v2 (_ BitVec 4))
(declare-const v3 (_ BitVec 4))
(declare-const v4 (_ BitVec 4))
(declare-const a2 (Array (_ BitVec 2) (_ BitVec 1) ))
(declare-const a3 (Array (_ BitVec 2) (_ BitVec 3) ))
(declare-const a4 (Array (_ BitVec 4) (_ BitVec 2) ))
(declare-const a5 (Array (_ BitVec 2) (_ BitVec 4) ))
(declare-const a6 (Array (_ BitVec 3) (_ BitVec 1) ))
(declare-const a7 (Array (_ BitVec 2) (_ BitVec 1) ))
(declare-const a8 (Array (_ BitVec 1) (_ BitVec 2) ))
(declare-const a9 (Array (_ BitVec 4) (_ BitVec 4) ))
(declare-const v5 (_ BitVec 4))
(declare-const v6 (_ BitVec 1))
(declare-const a10 (Array (_ BitVec 1) (_ BitVec 3) ))
(declare-const v7 (_ BitVec 3))
(declare-const a11 (Array (_ BitVec 1) (_ BitVec 3) ))
(declare-const a12 (Array (_ BitVec 2) (_ BitVec 2) ))
(declare-const a13 (Array (_ BitVec 1) (_ BitVec 1) ))
(declare-const v8 (_ BitVec 4))
(declare-const a14 (Array (_ BitVec 4) (_ BitVec 1) ))
(declare-const v9 (_ BitVec 1))
(declare-const a15 (Array (_ BitVec 3) (_ BitVec 2) ))
(declare-const v10 (_ BitVec 1))
(declare-const a16 (Array (_ BitVec 1) (_ BitVec 4) ))
(declare-const a17 (Array (_ BitVec 4) (_ BitVec 3) ))
(declare-const a18 (Array (_ BitVec 2) (_ BitVec 2) ))
(declare-const a19 (Array (_ BitVec 3) (_ BitVec 3) ))
(assert (= #b1 (bvnot (bvnor (ite (= (bvnand (bvor (bvnot (bvnot (bvor (bvredor (bvnot (select (store a0 v2 ((_ zero_extend 3) (ite (bvuge (bvnot ((_ sign_extend 2) (bvnot (bvnand ((_ extract 1 1) v0) ((_ extract 1 1) v0))))) ((_ sign_extend 2) (ite (bvugt (bvnot (_ bv0 1)) (ite (= ((_ extract 2 2) v7) ((_ extract 0 0) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2))))) #b1 #b0)) #b1 #b0))) #b1 #b0))) (bvsrem ((_ zero_extend 3) (ite (bvuaddo (bvnot v8) ((_ zero_extend 1) (bvnot v1))) #b1 #b0)) ((_ sign_extend 3) (ite (= ((_ extract 1 1) (bvnot (bvadd ((_ sign_extend 3) (bvnot v6)) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2)))))) ((_ extract 1 1) v0)) #b1 #b0)))))) (bvredand (select (store a11 (ite (bvsle ((_ sign_extend 2) (ite (bvugt (bvnot (_ bv0 1)) (ite (= ((_ extract 2 2) v7) ((_ extract 0 0) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2))))) #b1 #b0)) #b1 #b0)) ((_ sign_extend 2) (bvnot (ite (bvsge (select a11 (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5)))) v7) #b1 #b0)))) #b1 #b0) (bvnot ((_ sign_extend 2) (bvnot (ite (bvslt ((_ sign_extend 3) (bvnot v6)) (bvnot v8)) #b1 #b0))))) (bvredxor (bvnot ((_ sign_extend 1) (_ bv0 3))))))))) (bvxor (bvredor (select (store a15 (bvnot ((_ sign_extend 2) (_ bv0 1))) ((_ sign_extend 1) v6)) (bvnot ((_ extract 2 0) v3)))) (bvredor (select (store a16 (bvand (ite (bvsaddo (bvnot ((_ zero_extend 2) v6)) (bvnot v1)) #b1 #b0) v6) ((_ zero_extend 3) (ite (bvsle ((_ sign_extend 2) (ite (bvugt (bvnot (_ bv0 1)) (ite (= ((_ extract 2 2) v7) ((_ extract 0 0) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2))))) #b1 #b0)) #b1 #b0)) ((_ sign_extend 2) (bvnot (ite (bvsge (select a11 (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5)))) v7) #b1 #b0)))) #b1 #b0))) #b1)))) (bvand (bvnot (bvor (bvnot (bvredor (select (store a17 (bvnot v8) ((_ extract 2 0) (bvadd ((_ sign_extend 3) (bvnot v6)) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2)))))) (bvnot ((_ sign_extend 1) (bvnot (select a3 (bvnot ((_ extract 2 1) v5))))))))) (bvredxor (bvnot (select a18 ((_ extract 3 2) (bvnot v5))))))) (bvnand (bvredxor (select (store a19 (bvsub ((_ zero_extend 2) v6) ((_ extract 2 0) v3)) (bvurem (bvsub ((_ zero_extend 2) v6) ((_ extract 2 0) v3)) (select a3 (bvnot ((_ extract 2 1) v5))))) ((_ sign_extend 1) v0))) (bvnand (bvxor (bvxnor (bvor (ite (bvsmulo ((_ extract 2 1) v2) (bvnot ((_ extract 2 1) v2))) #b1 #b0) (_ bv0 1)) (bvor (ite (bvsmulo ((_ extract 2 1) v2) (bvnot ((_ extract 2 1) v2))) #b1 #b0) (_ bv0 1))) (_ bv0 1)) (ite (bvsmulo ((_ sign_extend 3) (bvnand ((_ extract 1 1) v0) ((_ extract 1 1) v0))) ((_ zero_extend 2) (bvudiv ((_ extract 2 1) (select a11 (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5))))) (bvnot ((_ extract 2 1) (select a11 (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5))))))))) #b1 #b0))))) (bvnot (bvnand (bvnand (bvnor (bvor (bvnot (ite (bvuge (bvnot ((_ sign_extend 3) (_ bv0 1))) ((_ zero_extend 3) v6)) #b1 #b0)) (bvnot (ite (bvusubo ((_ zero_extend 2) v6) ((_ sign_extend 1) v0)) #b1 #b0))) (bvxor (bvnot (ite (bvsgt (bvnot ((_ sign_extend 2) v9)) ((_ sign_extend 2) (bvnot (ite (bvslt ((_ sign_extend 3) (bvnot v6)) (bvnot v8)) #b1 #b0)))) #b1 #b0)) v10)) (bvnot (bvxor (bvor (bvnot #b1) (bvnot (ite (bvsge (bvnor ((_ extract 2 2) (bvnot (select a11 (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5)))))) ((_ extract 0 0) v5)) (ite (bvsge (select a11 (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5)))) v7) #b1 #b0)) #b1 #b0))) (bvxor (bvor (bvnot (ite (bvsle ((_ sign_extend 2) (ite (bvugt (bvnot (_ bv0 1)) (ite (= ((_ extract 2 2) v7) ((_ extract 0 0) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2))))) #b1 #b0)) #b1 #b0)) ((_ sign_extend 2) (bvnot (ite (bvsge (select a11 (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5)))) v7) #b1 #b0)))) #b1 #b0)) (ite (bvsgt (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 1) v7)) #b1 #b0)) (bvxor ((_ extract 0 0) v7) (ite (bvuaddo (bvnot v8) ((_ zero_extend 1) (bvnot v1))) #b1 #b0)))))) (bvnot (bvxor (bvxnor (ite (= (ite (bvsge ((_ sign_extend 1) (bvnot (select a3 (bvnot ((_ extract 2 1) v5))))) ((_ zero_extend 3) (select a14 ((_ zero_extend 3) (bvnot (bvor (ite (bvsmulo ((_ extract 2 1) v2) (bvnot ((_ extract 2 1) v2))) #b1 #b0) (_ bv0 1))))))) #b1 #b0) (bvnot (ite (bvusubo ((_ zero_extend 3) (ite (bvsle ((_ sign_extend 2) (ite (bvugt (bvnot (_ bv0 1)) (ite (= ((_ extract 2 2) v7) ((_ extract 0 0) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2))))) #b1 #b0)) #b1 #b0)) ((_ sign_extend 2) (bvnot (ite (bvsge (select a11 (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5)))) v7) #b1 #b0)))) #b1 #b0)) v4) #b1 #b0))) #b1 #b0) (bvnot (bvxnor (bvredxor (bvnot ((_ sign_extend 1) (_ bv0 3)))) (bvnot (bvnor (ite (bvsmulo (bvnot ((_ extract 3 1) v5)) ((_ sign_extend 2) (ite (bvsle (bvnot ((_ sign_extend 1) (ite (bvsle ((_ extract 2 2) v7) ((_ extract 3 3) v5)) #b1 #b0))) ((_ zero_extend 1) (ite (bvsmulo ((_ sign_extend 3) (bvnot v6)) ((_ sign_extend 3) (bvnot (ite (bvuge (bvnot ((_ sign_extend 2) (bvnot (bvnand ((_ extract 1 1) v0) ((_ extract 1 1) v0))))) ((_ sign_extend 2) (ite (bvugt (bvnot (_ bv0 1)) (ite (= ((_ extract 2 2) v7) ((_ extract 0 0) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2))))) #b1 #b0)) #b1 #b0))) #b1 #b0)))) #b1 #b0))) #b1 #b0))) #b1 #b0) (bvnot ((_ extract 0 0) (bvadd ((_ sign_extend 2) (bvnot (bvnand ((_ extract 1 1) v0) ((_ extract 1 1) v0)))) ((_ zero_extend 1) (bvnot v0)))))))))) (ite (or (or (not (bvslt v7 (bvnot ((_ zero_extend 2) (ite (= (store a14 v3 (ite (bvsmulo ((_ extract 2 1) v2) (bvnot ((_ extract 2 1) v2))) #b1 #b0)) (store a14 v3 (ite (bvsmulo ((_ extract 2 1) v2) (bvnot ((_ extract 2 1) v2))) #b1 #b0))) #b1 #b0))))) (bvsge v8 ((_ zero_extend 3) v6))) (xor (or (bvuaddo (bvnot (ite (bvsaddo (bvnot ((_ zero_extend 2) v6)) (bvnot v1)) #b1 #b0)) (bvnot ((_ extract 0 0) v5))) (bvsmulo ((_ sign_extend 3) (bvnot v6)) ((_ sign_extend 3) (bvnot (ite (bvuge (bvnot ((_ sign_extend 2) (bvnot (bvnand ((_ extract 1 1) v0) ((_ extract 1 1) v0))))) ((_ sign_extend 2) (ite (bvugt (bvnot (_ bv0 1)) (ite (= ((_ extract 2 2) v7) ((_ extract 0 0) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2))))) #b1 #b0)) #b1 #b0))) #b1 #b0))))) (= (bvnot (ite (bvsge (select a11 (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5)))) v7) #b1 #b0)) (bvnot ((_ extract 0 0) (bvnot v3)))))) #b1 #b0)))))) #b1 #b0) (bvnot (bvnand (bvor (bvnor (bvnot (bvnor (bvor (bvnot (bvmul ((_ extract 2 2) (bvnot #b011)) (ite (= ((_ extract 2 2) v7) ((_ extract 0 0) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2))))) #b1 #b0))) (bvnot (ite (bvuaddo ((_ extract 1 0) (bvnot v3)) ((_ extract 3 2) (bvnot v5))) #b1 #b0))) (bvxnor (ite (= (bvsaddo (bvnot ((_ zero_extend 2) v6)) (bvnot v1)) true) ((_ extract 1 1) (bvashr (bvnot ((_ extract 5 4) (concat v4 (bvnot ((_ zero_extend 2) (bvnot (bvor (ite (bvsmulo ((_ extract 2 1) v2) (bvnot ((_ extract 2 1) v2))) #b1 #b0) (_ bv0 1)))))))) ((_ zero_extend 1) (ite (= ((_ extract 2 2) v7) ((_ extract 0 0) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2))))) #b1 #b0)))) ((_ extract 0 0) (bvurem (bvsub ((_ zero_extend 2) v6) ((_ extract 2 0) v3)) (select a3 (bvnot ((_ extract 2 1) v5)))))) (select a1 ((_ extract 3 1) v5))))) (bvand (bvnot (bvor (bvnot (bvnot (select a2 (bvnot ((_ sign_extend 1) (ite (bvsgt (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 1) v7)) #b1 #b0)))))) (select a7 ((_ zero_extend 1) (ite (bvsmulo ((_ sign_extend 3) (bvnot v6)) ((_ sign_extend 3) (bvnot (ite (bvuge (bvnot ((_ sign_extend 2) (bvnot (bvnand ((_ extract 1 1) v0) ((_ extract 1 1) v0))))) ((_ sign_extend 2) (ite (bvugt (bvnot (_ bv0 1)) (ite (= ((_ extract 2 2) v7) ((_ extract 0 0) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2))))) #b1 #b0)) #b1 #b0))) #b1 #b0)))) #b1 #b0))))) (bvxnor (select (store a13 ((_ extract 1 1) v0) (_ bv0 1)) (ite (bvsgt (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 1) v7)) #b1 #b0)) (bvnot (select (store a13 (ite (bvule ((_ extract 1 1) v0) (bvnot (bvand (ite (bvsaddo (bvnot ((_ zero_extend 2) v6)) (bvnot v1)) #b1 #b0) v6))) #b1 #b0) ((_ extract 0 0) v7)) (ite (bvslt ((_ sign_extend 3) (bvnot v6)) (bvnot v8)) #b1 #b0)))))) (bvnot (bvor (bvnot (bvxor (ite (= (select (store a6 ((_ sign_extend 2) (_ bv0 1)) ((_ extract 1 1) (bvnot (bvudiv ((_ extract 2 1) (select a11 (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5))))) (bvnot ((_ extract 2 1) (select a11 (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5)))))))))) (bvurem (bvsub ((_ zero_extend 2) v6) ((_ extract 2 0) v3)) (select a3 (bvnot ((_ extract 2 1) v5))))) (bvredor (bvlshr (bvnot ((_ sign_extend 7) (bvand (ite (bvsaddo (bvnot ((_ zero_extend 2) v6)) (bvnot v1)) #b1 #b0) v6))) ((_ zero_extend 5) ((_ zero_extend 2) v6))))) #b1 #b0) (ite (= (bvredor ((_ sign_extend 3) (bvnot ((_ extract 2 1) v2)))) (bvredor ((_ zero_extend 4) (bvnot v1)))) #b1 #b0))) (bvor (bvnot (ite (= (bvredxor (select a4 ((_ sign_extend 3) (bvnot (ite (bvuge (bvnot ((_ sign_extend 2) (bvnot (bvnand ((_ extract 1 1) v0) ((_ extract 1 1) v0))))) ((_ sign_extend 2) (ite (bvugt (bvnot (_ bv0 1)) (ite (= ((_ extract 2 2) v7) ((_ extract 0 0) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2))))) #b1 #b0)) #b1 #b0))) #b1 #b0))))) (bvredxor (bvashr ((_ zero_extend 3) v6) ((_ zero_extend 2) (bvnot ((_ zero_extend 1) v9)))))) #b1 #b0)) (bvnor (bvredor (bvsrem v1 ((_ zero_extend 2) (bvand (ite (bvsaddo (bvnot ((_ zero_extend 2) v6)) (bvnot v1)) #b1 #b0) v6)))) (bvredor (_ bv0 2))))))) (bvand (ite (= (bvor (bvnot (bvnot (bvxor (bvredxor (bvshl ((_ sign_extend 12) (bvadd ((_ sign_extend 3) (bvnot v6)) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2))))) ((_ zero_extend 12) ((_ zero_extend 3) (bvnot (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5)))))))) (bvredxor (bvsrem ((_ extract 2 1) v5) ((_ sign_extend 1) (ite (bvuaddo (bvnot v8) ((_ zero_extend 1) (bvnot v1))) #b1 #b0))))))) (bvand (bvredor (bvneg (bvnot ((_ extract 5 2) (concat (bvnot ((_ zero_extend 1) v9)) v5))))) (bvredxor (bvurem ((_ sign_extend 1) v6) (bvnot ((_ extract 2 1) (bvsub ((_ zero_extend 2) v6) ((_ extract 2 0) v3)))))))) (bvand (bvnot (bvxor (bvredor (bvlshr (bvlshr ((_ sign_extend 12) (bvadd ((_ sign_extend 3) (bvnot v6)) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2))))) ((_ zero_extend 12) ((_ zero_extend 3) (bvnot (ite (bvsle ((_ sign_extend 2) (ite (bvugt (bvnot (_ bv0 1)) (ite (= ((_ extract 2 2) v7) ((_ extract 0 0) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2))))) #b1 #b0)) #b1 #b0)) ((_ sign_extend 2) (bvnot (ite (bvsge (select a11 (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5)))) v7) #b1 #b0)))) #b1 #b0))))) ((_ zero_extend 12) ((_ sign_extend 3) (bvnot (bvredxor ((_ extract 4 3) (concat v4 (bvnot ((_ zero_extend 2) (bvnot (bvor (ite (bvsmulo ((_ extract 2 1) v2) (bvnot ((_ extract 2 1) v2))) #b1 #b0) (_ bv0 1))))))))))))) (bvredand (bvnot (bvsub (bvnot ((_ sign_extend 1) v6)) ((_ sign_extend 1) (ite (bvsgt (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 1) v7)) #b1 #b0))))))) (bvnand (bvredand (bvsrem ((_ zero_extend 3) (ite (bvuaddo (bvnot v8) ((_ zero_extend 1) (bvnot v1))) #b1 #b0)) ((_ sign_extend 3) (ite (= ((_ extract 1 1) (bvnot (bvadd ((_ sign_extend 3) (bvnot v6)) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2)))))) ((_ extract 1 1) v0)) #b1 #b0)))) (bvredand (select a5 ((_ sign_extend 1) (ite (bvsmulo ((_ extract 2 1) v2) (bvnot ((_ extract 2 1) v2))) #b1 #b0))))))) #b1 #b0) (ite (= (bvxnor (bvnand (bvnot (bvredand (bvnot (select (store a10 ((_ extract 1 1) v0) (bvnot ((_ zero_extend 2) v6))) (bvand (ite (bvsaddo (bvnot ((_ zero_extend 2) v6)) (bvnot v1)) #b1 #b0) v6))))) (bvredxor (select (store a4 (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ extract 2 1) (select a11 (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5)))))) ((_ sign_extend 3) (ite (= ((_ extract 1 1) (bvnot (bvadd ((_ sign_extend 3) (bvnot v6)) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2)))))) ((_ extract 1 1) v0)) #b1 #b0))))) (bvxnor (bvredxor (select (store a3 ((_ sign_extend 1) (ite (bvsmulo ((_ extract 2 1) v2) (bvnot ((_ extract 2 1) v2))) #b1 #b0)) (bvnot ((_ extract 3 1) (bvnot v8)))) (bvurem ((_ sign_extend 1) v6) (bvnot ((_ extract 2 1) (bvsub ((_ zero_extend 2) v6) ((_ extract 2 0) v3))))))) (bvredand (select (store a8 ((_ extract 2 2) v7) ((_ extract 1 0) v7)) (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5))))))) (ite (= (bvnand (bvredxor (select (store a9 (bvnot ((_ zero_extend 2) (bvudiv ((_ extract 2 1) (select a11 (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5))))) (bvnot ((_ extract 2 1) (select a11 (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5))))))))) (bvashr (bvnot ((_ zero_extend 1) (bvnot v1))) ((_ zero_extend 2) ((_ extract 2 1) v2)))) v4)) (bvnot (bvredxor (select (store a4 ((_ sign_extend 3) (_ bv0 1)) ((_ sign_extend 1) (ite (bvsle ((_ extract 2 2) v7) ((_ extract 3 3) v5)) #b1 #b0))) v2)))) (bvnot (ite (= (bvnot (bvredor (select (store (store a12 ((_ extract 1 0) v7) ((_ extract 2 1) v2)) ((_ extract 2 1) (select a11 (bvnand ((_ extract 3 3) v5) (bvnand v6 ((_ extract 3 3) v5))))) ((_ sign_extend 1) (ite (bvsle ((_ extract 2 2) v7) ((_ extract 3 3) v5)) #b1 #b0))) ((_ extract 1 0) (bvnot v3))))) (bvredxor (bvnot (select (store a15 ((_ zero_extend 2) (_ bv0 1)) ((_ extract 3 2) (bvnot v5))) (bvnot ((_ sign_extend 2) v9)))))) #b1 #b0))) #b1 #b0)) #b1 #b0))))))))
(check-sat)