path: root/test/regress/regress0/issue1063-overloading-dt-fun.smt2

; EXPECT: sat
(set-logic ALL)
(set-info :status sat)
(declare-datatypes ((Enum 0)) (((cons (val Int)) (On_Ground) (None))))
(declare-fun cons (Int Int) Int)
(declare-fun cons (Enum) Bool)
(declare-fun cons (Bool) Int)
(assert (cons (cons 0)))
(assert (= (cons (cons true) (cons false)) 4))
(check-sat)