summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sygus/enum-test.sy
blob: 52a72c07d5642a71a0e391487963b3678ea13697 (plain) 
1
2
3
4
5
6
7
8

; EXPECT: unsat
; COMMAND-LINE: --cegqi-si
(set-logic LIA)
(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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback