diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-04-23 05:15:56 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-04-23 05:15:56 +0000 |
| commit | 57b8c4c8581d2d3ffcf3d3a1bb228271cb4d074a (patch) | |
| tree | 1c1781cc83118e4bbd2ad6939b16734c30a69f1a /test/regress/regress0 | |
| parent | 673d0e86b91094a58433c3ca71591fb0a0c60f84 (diff) | |
* reviewed BooleanSimplification, added documentation & unit test
* work around a lexer ambiguity in CVC grammar
* add support for tracing antlr parser/lexer
* add parsing support for more language features
* initial parameterized types parsing work to support Andy's work
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/subranges.cvc | 17 |
2 files changed, 18 insertions, 0 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 12e2bb347..323e61ca4 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -38,6 +38,7 @@ SMT2_TESTS = \ # Regression tests for PL inputs CVC_TESTS = \ + subranges.cvc \ boolean-prec.cvc \ hole6.cvc \ ite.cvc \ diff --git a/test/regress/regress0/subranges.cvc b/test/regress/regress0/subranges.cvc new file mode 100644 index 000000000..d8351c7f1 --- /dev/null +++ b/test/regress/regress0/subranges.cvc @@ -0,0 +1,17 @@ +% COMMAND-LINE: --parse-only +% EXPECT: +% EXIT: 0 + +A : [0..0]; +B : [ -5 .. 8]; +C : [1..3]; +D : [1..2]; +E : [-100 ..-1]; +F : [-100 ..0]; +G : [-100 ..1]; +H : [-1 ..1]; +I : [0..10]; +J : [-10..-9]; +J : [-10..-10]; + +QUERY TRUE; |