diff options
Diffstat (limited to 'test/regress/regress0/cvc3.userdoc.05.cvc')
| -rw-r--r-- | test/regress/regress0/cvc3.userdoc.05.cvc | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress0/cvc3.userdoc.05.cvc b/test/regress/regress0/cvc3.userdoc.05.cvc new file mode 100644 index 000000000..37da96b3c --- /dev/null +++ b/test/regress/regress0/cvc3.userdoc.05.cvc @@ -0,0 +1,14 @@ +x, y : BITVECTOR(4); + +ASSERT x = 0hex5; +ASSERT y = 0bin0101; + +% EXPECT: valid +QUERY + BVMULT(8,x,y)=BVMULT(8,y,x) + AND + NOT(BVLT(x,y)) + AND + BVLE(BVSUB(8,x,y), BVPLUS(8, x, BVUMINUS(x))) + AND + x = BVSUB(4, BVUMINUS(x), BVPLUS(4, x,0hex1)) ; |