blob: 1c0abc4fe54823673d91afa33b5d721334a77862 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-out=status
(set-logic BV)
(define-fun Spec ((k1 Bool) (k2 Bool) (k3 Bool) ) Bool
(xor k1 (and k3 (not k2)))
)
(synth-fun Imp ((k1 Bool) (k2 Bool) (k3 Bool)) Bool
((Start Bool) (d1 Bool) (d2 Bool))
((Start Bool ( (and d1 d1) (or d1 d1) (xor d1 d1) (not d1) ) )
(d1 Bool ( (and d2 d2) (or d2 d2) (xor d2 d2) (not d2) ) )
(d2 Bool ( k1 k2 k3) ) )
)
(declare-var k1 Bool)
(declare-var k2 Bool)
(declare-var k3 Bool)
(constraint (= (Spec k1 k2 k3) (Imp k1 k2 k3)))
(check-synth)
|
