diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-08 01:38:25 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-11 17:55:20 -0400 |
| commit | 21c71dd206b2b131ee12c811bd7b0997de07adfa (patch) | |
| tree | 29d98249bb8bba3c374adeee54621edcdc0bb977 /test/regress/regress0/bv | |
| parent | 463cf1b3ec4df9dff10026a2d306de2f41c9cef9 (diff) | |
Minor cleanup.
* Reenable parts of bvsimple test
* Fix typo in #endif comment
Diffstat (limited to 'test/regress/regress0/bv')
| -rw-r--r-- | test/regress/regress0/bv/bvsimple.cvc | 27 |
1 files changed, 12 insertions, 15 deletions
diff --git a/test/regress/regress0/bv/bvsimple.cvc b/test/regress/regress0/bv/bvsimple.cvc index be5707554..dcacd643a 100644 --- a/test/regress/regress0/bv/bvsimple.cvc +++ b/test/regress/regress0/bv/bvsimple.cvc @@ -22,22 +22,19 @@ QUERY ( 0bin0011 << 3 = 0bin0011000 ) AND ( 0bin1000 >> 3 = 0bin0001 ) AND -% these not working yet.. -% -%( 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 +( 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 |