diff options
Diffstat (limited to 'test/regress/regress0/bv/bvsimple.cvc')
-rw-r--r-- | test/regress/regress0/bv/bvsimple.cvc | 46 |
1 files changed, 0 insertions, 46 deletions
diff --git a/test/regress/regress0/bv/bvsimple.cvc b/test/regress/regress0/bv/bvsimple.cvc deleted file mode 100644 index 6bc649a03..000000000 --- a/test/regress/regress0/bv/bvsimple.cvc +++ /dev/null @@ -1,46 +0,0 @@ -% EXPECT: entailed - -% Some tests from the CVC3 user manual. -% http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html - -x : BITVECTOR(5); -y : BITVECTOR(4); -yy : BITVECTOR(3); - -bv : BITVECTOR(10); -a : BOOLEAN; - -xx : BITVECTOR(8); -zz : BITVECTOR(12); - -x4, y4 : BITVECTOR(4); - -QUERY -( 0bin0000111101010000 = 0hex0f50 ) AND -( 0bin01@0bin0 = 0bin010 ) AND -( 0bin1000 >> 3 = 0bin0001 ) AND -( 0bin0011 << 3 = 0bin0011000 ) AND -( 0bin1000 >> 3 = 0bin0001 ) AND - -( BVZEROEXTEND(0bin100, 2) = 0bin00100 ) AND -( SX(0bin100, 5) = 0bin11100 ) AND - -( BVZEROEXTEND(0bin100, 0) = 0bin100 ) AND -( SX(0bin100, 3) = 0bin100 ) AND - -( (BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11)))[8:4] = BVPLUS(5, x, ~(y[3:2])) ) AND - -( x4 = 0hex5 AND y4 = 0bin0101 ) => -( ( BVMULT(8,x4,y4)=BVMULT(8,y4,x4) ) AND - ( NOT(BVLT(x4,y4)) ) AND - ( BVLE(BVSUB(8,x4,y4), BVPLUS(8, x4, BVUMINUS(x4))) ) AND - ( x4 = BVSUB(4, BVUMINUS(x4), BVPLUS(4, x4,0hex1)) ) ) AND - -( 0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2] ) AND -( 0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF) = (IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0] ) AND - -( xx = 0hexff AND zz = 0hexff0 => - ( zz = xx << 4 ) AND - ( (zz >> 4)[7:0] = xx ) ) AND - -TRUE; |