path: root/test/regress/regress0/parser/as.smt2

(set-logic QF_UF)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status sat)
(declare-sort I 0)
(declare-fun e0 () I)

;; below we type cast e0 to its type
;; in other words, this just affirms that e0 has type I
;; previously, this was not handled correctly in the smt2 parser
(assert (= (as e0 I) (as e0 I)))

(check-sat)
(exit)