test/regress/regress1/sygus/issue3461.sy


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

; EXPECT: unsat
; COMMAND-LINE: --lang=sygus2 --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 Policy))
  ((Start Policy (Q))
   (Q Policy ((p 0) (p 1) (por Q Q))))
)

(check-synth)