path: root/test/regress/regress1/sygus/enum-test.sy

; EXPECT: unsat
; COMMAND-LINE: --cegqi-si=all --sygus-out=status
(set-logic LIA)
;; this is the custom enumeration datatype syntax from an early proposal of the sygus standard
(define-sort D (Enum (a b)))
(define-fun f ((x D)) Int (ite (= x D::a) 3 7))
(synth-fun g () D ((Start D (D::a D::b))))
(constraint (= (f g) 7))
(check-synth)