1 2 3 4 5 6 7 8 9 10
; 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)