blob: f2b28db9c890ee80f63b5191843431b4e8390fb2 (
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
39
40
41
42
43
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status
(set-logic BV)
(define-fun origCir ( (LN4 Bool) (LN91 Bool) ) Bool
(and LN91 LN4 )
)
(synth-fun skel ( (LN4 Bool) (LN91 Bool) ) Bool
((Start Bool (
(and depth1 depth1)
(xor depth1 depth1)
))
(depth1 Bool (
(not depth2)
LN91
))
(depth2 Bool (
(and depth3 depth3)
(not depth3)
(or depth3 depth3)
))
(depth3 Bool (
(and depth4 depth4)
(not depth4)
(or depth4 depth4)
(xor depth4 depth4)
))
(depth4 Bool (
LN4
)))
)
(declare-var LN4 Bool)
(declare-var LN91 Bool)
(constraint (= (origCir LN4 LN91 ) (skel LN4 LN91 )))
(check-synth)
|