blob: 6aa17ef307e2406f9d0228bdad66d131c5a37939 (
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
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-unif-pi=complete --sygus-out=status
(set-logic BV)
(synth-fun f ((x (_ BitVec 64)) (y (_ BitVec 64))) (_ BitVec 64)
((Start (_ BitVec 64)) (CBool Bool))
(
(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)
|