test/regress/regress1/sygus/issue3461.sy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status

(set-logic ALL_SUPPORTED)

(declare-datatype Doc ((D (owner Int) (body Int))))

(declare-datatype Policy 
  ((p (principal Int)) 
   (por (left Policy) (right Policy))))

(synth-fun mkPolicy ((d Doc)) Policy
  ((Start Policy (Q))
   (Q Policy ((p 0) (p 1) (por Q Q))))
)

(check-synth)