blob: 63cc4736cbc2767299a791fd46ebf5a471148a40 (
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
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --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)) (StartBool Bool))
((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)
|
