From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Tue, 4 May 2010 22:27:40 +0000 (+0000)
Subject: Adding simple SMT2 parser tests
X-Git-Tag: cvc5-1.0.0~9079
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fec2b5751108088ff651ce6eed09bf3aa65f281e;p=cvc5.git

Adding simple SMT2 parser tests
---

diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 0389a75ef..b8060086f 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -149,8 +149,10 @@ const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string);
 const string goodSmt2Inputs[] = {
     "", // empty string is OK
     "(set-logic QF_UF)",
+    "(set-info :notes |This is a note, take note!|)",
     "(assert true)",
     "(check-sat)",
+    "(exit)",
     "(assert false) (check-sat)",
     "(declare-fun a () Bool) (declare-fun b () Bool)",
     "(declare-fun a () Bool) (declare-fun b () Bool) (assert (=> (and (=> a b) a) b))",
@@ -179,6 +181,7 @@ const int numGoodSmt2Exprs = sizeof(goodSmt2Exprs) / sizeof(string);
 
 const string badSmt2Inputs[] = {
     "(assert)", // no args
+    "(set-info :notes |Symbols can't contain the | character|)",
     "(check-sat true)", // shouldn't have an arg
     "(declare-sort a)", // no arg
     "(declare-sort a 0) (declare-sort a 0)", // double decl