blob: f0cbbdc534b5c0661dbc7b83f6be0cb06fdc9dab (
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
|
; 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)
(ite StartBool Start Start)
))
(StartBool Bool ((= Start #x0000000000000001)))
)
)
(constraint (= (f #x0000000000000001) #x0000000000000001))
(constraint (= (f #x0000000000100001) #x0000000000100001))
(constraint (= (f #xE5D371D100002E8A) #x0000000000000000))
(check-synth)
|
