blob: 6b647b77dbb17bd7a84a341c281e7ca8845cbe62 (
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
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-unif-pi=complete --sygus-out=status
(set-logic BV)
(synth-fun f ((x (BitVec 64)) (y (BitVec 64))) (BitVec 64)
(
(Start (BitVec 64)
(#x0000000000000000 #x0000000000000001 x y
(bvnot Start)
(bvand Start Start)
(bvor Start Start)
(bvxor Start Start)
(bvadd Start Start)
(ite CBool Start Start)
)
)
(CBool Bool
(true false
(and CBool CBool)
(or CBool CBool)
(not CBool)
(bvule Start Start)
(= Start Start)
)
)
)
)
(declare-var x (BitVec 64))
(declare-var y (BitVec 64))
(constraint (= (f #x0000000000000000 #x0000000000000001) #x0000000000000000))
(constraint (= (f #x0000000000000000 #x0000000000000000) #x0000000000000001))
(constraint (= (f #x0000000000000001 y) y))
(constraint (= (f #x0000000000000002 #x0000000000000001) #x0000000000000000))
(check-synth)
|
