blob: 70cb6b2d2597887a5c6c5af0a8154b48d0fd6eab (
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
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(set-logic BV)
(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))
(synth-fun f ( (x (BitVec 64))) (BitVec 64)
(
(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
(shl1 Start)
(shr1 Start)
(shr4 Start)
(shr16 Start)
(bvand Start Start)
(bvor Start Start)
(bvxor Start Start)
(bvadd Start Start)
(if0 Start Start Start)
))
)
)
(constraint (= (f #x9db91b67d1eee4b4) #x00009db91b67d1ee))
(constraint (= (f #x211526232b50ea1d) #xdeead9dcd4af15e2))
(constraint (= (f #xedcec1de604e94ec) #x0000edcec1de604e))
(constraint (= (f #xede1841179ee3684) #x0000ede1841179ee))
(constraint (= (f #x9c623bcc40d252bd) #x639dc433bf2dad42))
(constraint (= (f #x4601c6d84a50d01b) #xb9fe3927b5af2fe4))
(constraint (= (f #x0c5ed1e748c4e26c) #x00000c5ed1e748c4))
(constraint (= (f #x6bb653229e60ee94) #x00006bb653229e60))
(constraint (= (f #x483db90b3dee6596) #x0000483db90b3dee))
(constraint (= (f #x55376e703c4a1ea8) #x000055376e703c4a))
(synth-fun g ( (x (BitVec 64))) (BitVec 64)
(
(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
(shl1 Start)
(shr1 Start)
(shr4 Start)
(shr16 Start)
(bvand Start Start)
(bvor Start Start)
(bvxor Start Start)
(bvadd Start Start)
(if0 Start Start Start)
))
)
)
(constraint (= (g #xd5a6481ee2ba1030) #xfffffffffffffffe))
(constraint (= (g #x03e887e72dee55cd) #x03e887e72dee55cd))
(constraint (= (g #xaced92921c8e318d) #xaced92921c8e318d))
(constraint (= (g #x95e5e4184e40aaec) #xfffffffffffffffe))
(constraint (= (g #x352367e34d76550b) #x352367e34d76550b))
(constraint (= (g #x398560eeee7b1b6c) #xfffffffffffffffe))
(constraint (= (g #x099be4899986c29a) #xfffffffffffffffe))
(constraint (= (g #xb14b75be2e13445a) #xfffffffffffffffe))
(constraint (= (g #xb4c680ad7e6b16ce) #xfffffffffffffffe))
(constraint (= (g #x7e4954872868acb8) #xfffffffffffffffe))
(check-synth)
|
