From 3cb49313dbefe6111414dafa521e006d45eb72d8 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Thu, 29 Apr 2010 19:45:21 +0000 Subject: Minor fix to SMT v2 parser tests --- test/unit/parser/parser_black.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'test') 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" }; -- cgit v1.2.3