test/regress/regress1/sygus/crci-ssb-unk.sy


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)