diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-07 00:01:13 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-07 00:01:13 +0000 |
commit | 868d2f9cf7c8dcdee6dbf7d88b4d002065e8ae68 (patch) | |
tree | d905c11c5cb087c624be564d7815e930339150d9 /test/regress/regress0/precedence/cmp-plus.cvc | |
parent | 481c564c68b83925355c82e2d18ade8f1b3fa4db (diff) |
Adding tests for precedence of arithmetic in CVC inputs
Diffstat (limited to 'test/regress/regress0/precedence/cmp-plus.cvc')
-rw-r--r-- | test/regress/regress0/precedence/cmp-plus.cvc | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test/regress/regress0/precedence/cmp-plus.cvc b/test/regress/regress0/precedence/cmp-plus.cvc new file mode 100644 index 000000000..af2823fcf --- /dev/null +++ b/test/regress/regress0/precedence/cmp-plus.cvc @@ -0,0 +1,8 @@ +% EXPECT: VALID +% Simple test for right precedence of comparisons and plus/minus + +x, y, z: INT; + +QUERY (x + y - z > 0 AND 0 < x - y + z) <=> + ((((x + y) - z) > 0) AND (0 < ((x - y) + z))); +% EXIT: 20 |