test/regress/regress0/issue1063-overloading-dt-sel.smt2

   1 ; COMMAND-LINE: --lang=smt2.5
   2 ; EXPECT: sat
   3 (set-logic ALL)
   4 (set-info :status sat)
   5 (declare-datatypes () ((Enum0 (cons (data Int)) (None))))
   6 (declare-datatypes () ((Enum1 (cons (data Bool)) (None))))
   7 (declare-fun var_0 () Enum0)
   8 (declare-fun var_1 () Enum1)
   9 (assert (= (data var_0) 5))
  10 (assert (data var_1))
  11 (check-sat)