diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-04-27 20:44:47 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-04-27 20:44:47 +0000 |
commit | 0c4a6edae95b3ffc76cb82604a3d1694d42625bb (patch) | |
tree | 38cf873c7fac5e1e25529425f4835aac3d79adbb /test | |
parent | 130b814916c096f4b898a26c9df5056270af78d0 (diff) |
Adding Integer and Rational constants to SMT
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/parser/parser_white.h | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/test/unit/parser/parser_white.h b/test/unit/parser/parser_white.h index 317817e15..1d19525d6 100644 --- a/test/unit/parser/parser_white.h +++ b/test/unit/parser/parser_white.h @@ -109,7 +109,10 @@ const string goodSmtExprs[] = { "(and (iff a b) (not a))", "(iff (xor a b) (and (or a b) (not (and a b))))", "(ite a (f x) y)", - "(if_then_else a (f x) y)" + "(if_then_else a (f x) y)", + "1", + "0"// , +// "1.5" }; const int numGoodSmtExprs = sizeof(goodSmtExprs) / sizeof(string); @@ -134,7 +137,9 @@ const string badSmtExprs[] = { "(not a b)", // wrong arity "not a", // needs parens "(ite a x)", // wrong arity - "(a b)" // using non-function as function + "(a b)", // using non-function as function + ".5", // rational constants must have integer prefix + "1." // rational constants must have fractional suffix }; const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string); |