diff options
Diffstat (limited to 'Test/bitvectors/bv8.bpl')
-rw-r--r-- | Test/bitvectors/bv8.bpl | 50 |
1 files changed, 25 insertions, 25 deletions
diff --git a/Test/bitvectors/bv8.bpl b/Test/bitvectors/bv8.bpl index ee572998..557eb4e8 100644 --- a/Test/bitvectors/bv8.bpl +++ b/Test/bitvectors/bv8.bpl @@ -1,25 +1,25 @@ -// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// This file includes some tests for which Boogie once generated bad Z3 input
-
-procedure foo()
-{
- var r: bv3;
- var s: bv6;
- var u: bv15;
- var t: bv24;
-
- t := t[8: 0] ++ t[10: 0] ++ t[24: 18];
- t := (r ++ s) ++ u;
- t := t[16: 0] ++ t[8: 0];
-}
-
-procedure bar()
-{
- var a: bv64;
- var b: bv32;
- var c: bv8;
-
- c := a[8:0];
- c := b[8:0];
-}
+// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// This file includes some tests for which Boogie once generated bad Z3 input + +procedure foo() +{ + var r: bv3; + var s: bv6; + var u: bv15; + var t: bv24; + + t := t[8: 0] ++ t[10: 0] ++ t[24: 18]; + t := (r ++ s) ++ u; + t := t[16: 0] ++ t[8: 0]; +} + +procedure bar() +{ + var a: bv64; + var b: bv32; + var c: bv8; + + c := a[8:0]; + c := b[8:0]; +} |