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, 0 insertions, 14 deletions
diff --git a/test/regress/regress0/cvc3.userdoc.05.cvc b/test/regress/regress0/cvc3.userdoc.05.cvc deleted file mode 100644 index 85e0c2105..000000000 --- a/test/regress/regress0/cvc3.userdoc.05.cvc +++ /dev/null @@ -1,14 +0,0 @@ -x, y : BITVECTOR(4); - -ASSERT x = 0hex5; -ASSERT y = 0bin0101; - -% EXPECT: entailed -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)) ; |