blob: ebf103c8557b2a63e6423db4a0566088d089ae3f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
(set-logic ALL)
(set-info :status sat)
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 4)))
(declare-fun b () (Array (_ BitVec 32) (_ BitVec 4)))
(declare-fun o () (_ BitVec 1))
(declare-fun h () (_ BitVec 32))
(declare-fun i () (_ BitVec 32))
(declare-fun j () (_ BitVec 32))
(declare-fun l () (_ BitVec 32))
(declare-fun m () (_ BitVec 32))
(assert (= (_ bv1 1) (bvmul (ite (= (_ bv1 1) (ite (= h (_ bv0 32)) (_ bv1 1)
(_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnor (bvcomp o (ite (= l (bvor ((_
zero_extend 28) (select b (bvadd i (_ bv3 32)))) (bvlshr ((_ zero_extend 28)
(select b (bvudiv i (_ bv1 32)))) ((_ zero_extend 28) (select b (bvadd i (_
bv2 32))))))) (_ bv1 1) (_ bv0 1))) (bvsmod (ite (= (_ bv0 1) (ite (= i (_
bv1 32)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvshl (ite (= (_ bv1 1)
(ite (= b (store (store (store (store a (bvadd j (_ bv3 32)) (_ bv0 4))
(bvsdiv j (_ bv2 32)) (_ bv1 4)) (bvadd j (_ bv1 32)) (_ bv0 4)) j ((_
extract 3 0) l))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (ite (= (_ bv0
32) (bvor ((_ zero_extend 28) (select a (bvadd m (_ bv3 32)))) (bvadd (bvor
((_ zero_extend 28) (select a (bvadd m (_ bv1 32)))) ((_ zero_extend 28)
(select a (bvnor m (_ bv0 32))))) ((_ zero_extend 28) (select a (bvadd m (_
bv2 32))))))) (_ bv1 1) (_ bv0 1))))))))
(check-sat)
|
