blob: f1807fd8f0e6c103cbbb5c1dcaa3e67b2b6ed492 (
plain)
1
2
3
4
5
6
7
|
(set-option :incremental false)
(set-info :status unsat)
(set-logic QF_AUFBV)
(declare-fun start2 () (_ BitVec 32))
(declare-fun start1 () (_ BitVec 32))
(declare-fun a1 () (Array (_ BitVec 32) (_ BitVec 8)))
(check-sat-assuming ( (let ((_let_0 (store (store a1 start1 (_ bv0 8)) (bvadd (_ bv3 32) start1) (_ bv0 8)))) (let ((_let_1 (select _let_0 (_ bv1 32)))) (let ((_let_2 (select _let_0 (_ bv0 32)))) (let ((_let_3 (bvand (bvnot (bvand (bvnot _let_1) (bvnot _let_2))) (bvnot (bvand _let_1 _let_2))))) (let ((_let_4 (bvand (bvnot (bvand (bvnot _let_1) (bvnot _let_3))) (bvnot (bvand _let_1 _let_3))))) (let ((_let_5 (store (store _let_0 (_ bv1 32) _let_4) (_ bv0 32) (bvand (bvnot (bvand (bvnot _let_3) (bvnot _let_4))) (bvnot (bvand _let_3 _let_4)))))) (let ((_let_6 (bvadd (_ bv3 32) start2))) (let ((_let_7 (select _let_5 _let_6))) (let ((_let_8 (select _let_5 start2))) (let ((_let_9 (bvand (bvnot (bvand (bvnot _let_7) (bvnot _let_8))) (bvnot (bvand _let_7 _let_8))))) (let ((_let_10 (bvand (bvnot (bvand (bvnot _let_7) (bvnot _let_9))) (bvnot (bvand _let_7 _let_9))))) (let ((_let_11 (store (store _let_5 _let_6 _let_10) start2 (bvand (bvnot (bvand (bvnot _let_9) (bvnot _let_10))) (bvnot (bvand _let_9 _let_10)))))) (let ((_let_12 (select _let_11 (_ bv0 32)))) (let ((_let_13 (select _let_11 start2))) (let ((_let_14 (bvand (bvnot (bvand (bvnot _let_12) (bvnot _let_13))) (bvnot (bvand _let_12 _let_13))))) (let ((_let_15 (bvand (bvnot (bvand (bvnot _let_12) (bvnot _let_14))) (bvnot (bvand _let_12 _let_14))))) (let ((_let_16 (store (store _let_11 (_ bv0 32) _let_15) start2 (bvand (bvnot (bvand (bvnot _let_14) (bvnot _let_15))) (bvnot (bvand _let_14 _let_15)))))) (let ((_let_17 (select _let_16 (_ bv1 32)))) (let ((_let_18 (select _let_16 (_ bv0 32)))) (let ((_let_19 (bvand (bvnot (bvand (bvnot _let_17) (bvnot _let_18))) (bvnot (bvand _let_17 _let_18))))) (let ((_let_20 (bvand (bvnot (bvand (bvnot _let_17) (bvnot _let_19))) (bvnot (bvand _let_17 _let_19))))) (let ((_let_21 (store (store a1 (bvadd (_ bv3 32) start1) (_ bv0 8)) start1 (_ bv0 8)))) (let ((_let_22 (store (store _let_21 (_ bv1 32) (select _let_21 (_ bv0 32))) (_ bv0 32) (select _let_21 (_ bv1 32))))) (let ((_let_23 (store (store _let_22 _let_6 (select _let_22 start2)) start2 (select _let_22 _let_6)))) (let ((_let_24 (store (store _let_23 (_ bv0 32) (select _let_23 start2)) start2 (select _let_23 (_ bv0 32))))) (not (= (_ bv0 1) (bvnot (ite (= (store (store _let_16 (_ bv1 32) _let_20) (_ bv0 32) (bvand (bvnot (bvand (bvnot _let_19) (bvnot _let_20))) (bvnot (bvand _let_19 _let_20)))) (store (store _let_24 (_ bv1 32) (select _let_24 (_ bv0 32))) (_ bv0 32) (select _let_24 (_ bv1 32)))) (_ bv1 1) (_ bv0 1)))))))))))))))))))))))))))))) ))
|
