Add regression from #50 regarding "as" parsing in smt2 (#1188)

* Add regression from pull request #50, which was fixed separately in pull request #1162.

* Improve comment in regression

diff --git a/test/regress/regress0/parser/Makefile.am b/test/regress/regress0/parser/Makefile.am
index ab91679438408711f976159296ec1203ea928306..c1b80b5ff44606f231a69f180875239ee05e60f4 100644 (file)
--- a/test/regress/regress0/parser/Makefile.am
+++ b/test/regress/regress0/parser/Makefile.am
@@ -22,7 +22,8 @@ TESTS =       \
        declarefun-emptyset-uf.smt2 \
        constraint.smt2 \
        strings20.smt2 \
-       strings25.smt2
+       strings25.smt2 \
+       as.smt2
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress0/parser/as.smt2 b/test/regress/regress0/parser/as.smt2
new file mode 100644 (file)
index 0000000..2ba6895
--- /dev/null
+++ b/test/regress/regress0/parser/as.smt2
@@ -0,0 +1,14 @@
+(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)