From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Thu, 29 Apr 2010 19:45:21 +0000 (+0000)
Subject: Minor fix to SMT v2 parser tests
X-Git-Tag: cvc5-1.0.0~9098
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3cb49313dbefe6111414dafa521e006d45eb72d8;p=cvc5.git

Minor fix to SMT v2 parser tests
---

diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index b7fbf243f..0389a75ef 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -154,8 +154,8 @@ const string goodSmt2Inputs[] = {
     "(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))",
-    "(declare-sort a 1) (declare-fun f (a) a) (declare-fun x () a) (assert (= (f x) x))",
-    "(declare-sort a 1) (declare-fun x () a) (declare-fun y () a) (assert (= (ite true x y) x))",
+    "(declare-sort a 0) (declare-fun f (a) a) (declare-fun x () a) (assert (= (f x) x))",
+    "(declare-sort a 0) (declare-fun x () a) (declare-fun y () a) (assert (= (ite true x y) x))",
     ";; nothing but a comment",
     "; a comment\n(check-sat ; goodbye\n)"
   };
@@ -181,7 +181,7 @@ const string badSmt2Inputs[] = {
     "(assert)", // no args
     "(check-sat true)", // shouldn't have an arg
     "(declare-sort a)", // no arg
-    "(declare-sort a 1) (declare-sort a 1)", // double decl
+    "(declare-sort a 0) (declare-sort a 0)", // double decl
     "(declare-fun p Bool)" // should be "p () Bool"
   };