diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-04-29 19:45:21 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-04-29 19:45:21 +0000 |
| commit | 3cb49313dbefe6111414dafa521e006d45eb72d8 (patch) | |
| tree | a50305f493fc311ecbfb0032337c48d1692c692d | |
| parent | 194c5b6f04c7c9bec8c0f23b88ac8d0f0094186a (diff) | |
Minor fix to SMT v2 parser tests
| -rw-r--r-- | test/unit/parser/parser_black.h | 6 |
1 files changed, 3 insertions, 3 deletions
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" }; |