; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status --lang=sygus2 --sygus-active-gen=enum

(set-logic ALL)

(declare-datatype Formula (
  (P (Id Int))
  (Op1 (op1 Int) (f Formula))
  (Op2 (op2 Int) (f1 Formula) (f2 Formula))
  )
)

(synth-fun phi () Formula
  ((<F> Formula) (<O2> Int))
  ((<F> Formula (
     (P <O2>)
     (Op1 <O2> <F>)
     (Op2 <O2> <F> <F>)
     )
   )
   (<O2> Int (0 1))
   )
)
(define-fun holds ((f Formula)) Bool
  (and ((_ is Op2) f) (= (op2 f) 1))
)
(define-fun holds2 ((f Formula)) Bool
  (and ((_ is Op2) f) (= (op1 (f1 f)) 1))
)
(constraint (holds phi))
(check-synth)