blob: 02f7754cf33c552e5495444a64f0076a66d8fc94 (
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
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
; COMMAND-LINE: --check-models
; EXPECT: sat
(set-logic QF_ABV)
(declare-fun c () (_ BitVec 32))
(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun b () (_ BitVec 32))
(assert (let ((a!1 (bvxnor (concat #x000000 (select a (bvadd c #x00000001))) #x00000008))
(a!3 (bvsdiv (concat #x000000 (select a (bvadd c #x00000002))) #x00000010))
(a!4 (bvudiv (concat #x000000 (select a (bvashr c #x00000003)))
#x00000018))
(a!5 (select a
(bvxor (bvsub (bvnand c #x00000004) #x00000004) #x00000000)))
(a!6 (select a
(bvsdiv (bvsub (bvnand c #x00000004) #x00000004) #x00000001)))
(a!7 (select a
(bvadd (bvsub (bvnand c #x00000004) #x00000004) #x00000002)))
(a!9 (store a
(bvashr (bvurem (bvnand c #x00000004) #x00000004) #x00000001)
((_ extract 7 0) (bvxnor b #x00000008))))
(a!11 (bvnand (bvurem (bvsub (bvnand c #x00000004) #x00000004) #x00000004)
#x00000008)))
(let ((a!2 (bvnor (concat #x000000 (select a (bvsmod c #x00000000))) a!1))
(a!8 (bvlshr (bvor (concat #x000000 a!5)
(bvmul (concat #x000000 a!6) #x00000008))
(bvand (concat #x000000 a!7) #x00000010)))
(a!10 (store a!9
(bvshl (bvurem (bvnand c #x00000004) #x00000004) #x00000000)
((_ extract 7 0) b)))
(a!12 (bvsub (concat #x000000 (select a (bvashr a!11 #x00000001)))
#x00000008))
(a!14 (bvxnor (concat #x000000 (select a (bvxnor a!11 #x00000002)))
#x00000010))
(a!15 (bvxor (concat #x000000 (select a (bvsub a!11 #x00000003)))
#x00000018)))
(let ((a!13 (bvor (concat #x000000 (select a (bvmul a!11 #x00000000))) a!12)))
(let ((a!16 ((_ extract 7 0)
(bvmul (bvurem (bvurem a!13 a!14) a!15) #x00000018)))
(a!17 ((_ extract 7 0) (bvor (bvurem (bvurem a!13 a!14) a!15) #x00000010)))
(a!18 ((_ extract 7 0)
(bvnor (bvurem (bvurem a!13 a!14) a!15) #x00000008))))
(let ((a!19 (store (store (store (store a!10 #x08053e77 a!16) #x08053e76 a!17)
#x08053e75
a!18)
#x08053e74
((_ extract 7 0) (bvurem (bvurem a!13 a!14) a!15)))))
(let ((a!20 (select a!19
(bvadd (bvsub (bvnand c #x00000004) #x00000004) #x00000003))))
(let ((a!21 (distinct (bvsdiv (bvsmod a!2 a!3) a!4)
(bvshl a!8 (bvshl (concat #x000000 a!20) #x00000018)))))
(= #b1 (bvashr (ite (or a!21) #b1 #b0) #b1))))))))))
(check-sat)
|
