summaryrefslogtreecommitdiff
path: root/Test/bitvectors/bv2.bpl
diff options
context:
space:
mode:
authorGravatar Checkmate50 <dgeisler50@gmail.com>2016-06-06 23:14:18 -0600
committerGravatar Checkmate50 <dgeisler50@gmail.com>2016-06-06 23:14:18 -0600
commitd652155ae013f36a1ee17653a8e458baad2d9c2c (patch)
tree067d600fe3cd1723afc11682935f0123a1eab653 /Test/bitvectors/bv2.bpl
parentd7fc0deb2ca6d7ebee094b6ea5430d9b41f163ec (diff)
Merging complete. Everything looks good *crosses fingers*
Diffstat (limited to 'Test/bitvectors/bv2.bpl')
-rw-r--r--Test/bitvectors/bv2.bpl26
1 files changed, 13 insertions, 13 deletions
diff --git a/Test/bitvectors/bv2.bpl b/Test/bitvectors/bv2.bpl
index 45fdf7e4..8e2c1dad 100644
--- a/Test/bitvectors/bv2.bpl
+++ b/Test/bitvectors/bv2.bpl
@@ -1,13 +1,13 @@
-// RUN: %boogie -proverWarnings:1 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure foo2(x : bv32) returns(r : bv32)
-{
- block1:
- r := x[-1:1]; // Error
-// r := x[x:1]; // Error
- r := x[1:x]; // Error
- r := x[1+1:3]; // Error
- return;
-}
-
-
+// RUN: %boogie -proverWarnings:1 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo2(x : bv32) returns(r : bv32)
+{
+ block1:
+ r := x[-1:1]; // Error
+// r := x[x:1]; // Error
+ r := x[1:x]; // Error
+ r := x[1+1:3]; // Error
+ return;
+}
+
+