blob: 212ae37f5ea2faf6ca12bed78473386dcfb8faad (
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
|
; 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 #xd74594057974e439) #x0000d74594057974))
(constraint (= (f #x74641ebeee92e8a2) #x000074641ebeee92))
(constraint (= (f #x91c80141d7ec76b1) #x000091c80141d7ec))
(constraint (= (f #xe4e55862e5ee4bec) #x0000e4e55862e5ee))
(constraint (= (f #x367da67ede4260ce) #x0000367da67ede42))
(constraint (= (f #xa365eb36246b3d8e) #x0000a365eb36246b))
(constraint (= (f #xcd8a44a6d4c09c29) #x0000cd8a44a6d4c0))
(constraint (= (f #xa97e9b9b7970433d) #x0000a97e9b9b7970))
(constraint (= (f #x474dec0dd75d6894) #x0000474dec0dd75d))
(constraint (= (f #x12430014ed058b24) #x000012430014ed05))
(check-synth)
|
