; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --sygus-si-rcons=try --sygus-out=status

(set-logic BV)


(define-fun origCir ( (LN24 Bool) (k3 Bool) (LN129 Bool) (LN141 Bool)  )  Bool    
          (not (not (not (xor (not (xor (not (and  LN24 k3 ) ) LN129 ) ) LN141 ) ) ) )
)


(synth-fun skel ( (LN24 Bool) (k3 Bool) (LN129 Bool) (LN141 Bool)  )  Bool    
          ((Start Bool) (depth1 Bool) (depth2 Bool) (depth3 Bool) (depth4 Bool)
           (depth5 Bool) (depth6 Bool) (depth7 Bool) (depth8 Bool))
          ((Start Bool (
		                                  (and depth1 depth1)
		                                  (not depth1)
		                                  (or depth1 depth1)
		                                  (xor depth1 depth1)
          ))
          (depth1 Bool (
		                                  (and depth2 depth2)
		                                  (not depth2)
		                                  (or depth2 depth2)
		                                  (xor depth2 depth2)
          ))
          (depth2 Bool (
		                                  (and depth3 depth3)
		                                  (not depth3)
		                                  (or depth3 depth3)
		                                  (xor depth3 depth3)
          ))
          (depth3 Bool (
		                                  (and depth4 depth4)
		                                  (not depth4)
		                                  (or depth4 depth4)
		                                  (xor depth4 depth4)
          ))
          (depth4 Bool (
		                                  (and depth5 depth5)
		                                  (not depth5)
		                                  (or depth5 depth5)
		                                  (xor depth5 depth5)
		                                  LN141
          ))
          (depth5 Bool (
		                                  (and depth6 depth6)
		                                  (not depth6)
		                                  (or depth6 depth6)
		                                  (xor depth6 depth6)
          ))
          (depth6 Bool (
		                                  (and depth7 depth7)
		                                  (not depth7)
		                                  (or depth7 depth7)
		                                  (xor depth7 depth7)
		                                  LN129
          ))
          (depth7 Bool (
		                                  (and depth8 depth8)
		                                  (not depth8)
		                                  (or depth8 depth8)
		                                  (xor depth8 depth8)
		                                  LN24
          ))
          (depth8 Bool (
		                                  k3
          )))
)


(declare-var LN24 Bool)
(declare-var k3 Bool)
(declare-var LN129 Bool)
(declare-var LN141 Bool)

(constraint (= (origCir LN24 k3 LN129 LN141 ) (skel LN24 k3 LN129 LN141 )))


(check-synth)