3 files changed, 103 insertions, 103 deletions
diff --git a/Test/test7/MultipleErrors.bpl b/Test/test7/MultipleErrors.bpl
index 6f5944fc..8d07841a 100644
--- a/Test/test7/MultipleErrors.bpl
+++ b/Test/test7/MultipleErrors.bpl
@@ -1,38 +1,38 @@
-// RUN: %boogie -vc:block -errorLimit:1 -errorTrace:1 -logPrefix:-1block "%s" > "%t1"
-// RUN: %diff "%s.e1.block.expect" "%t1"
-// RUN: %boogie -vc:local -errorLimit:1 -errorTrace:1 -logPrefix:-1local "%s" > "%t2"
-// RUN: %diff "%s.e1.local.expect" "%t2"
-// RUN: %boogie -vc:dag -errorLimit:1 -errorTrace:1 -logPrefix:-1dag "%s" > "%t3"
-// RUN: %diff "%s.e1.dag.expect" "%t3"
-// RUN: %boogie -vc:local -errorLimit:10 -errorTrace:1 -logPrefix:-10local "%s" > "%t4"
-// RUN: %diff "%s.e10.local.expect" "%t4"
-// RUN: %boogie -vc:dag -errorLimit:10 -errorTrace:1 -logPrefix:-10dag "%s" > "%t5"
-// RUN: %diff "%s.e10.dag.expect" "%t5"
-
-// Author of this comment: mikebarnett ec02177eefb5
-// The following tests are rather fickle at the moment--different errors
-// may be reported during different runs.  Moreover, it is conceivable that
-// the error trace would be reported in different orders, since we do not
-// attempt to sort the trace labels at this time.
-// An interesting thing is that /vc:local can with Simplify report more than one
-// error for this file, even with /errorLimit:1.  Other than that, only
-// local and dag produce VCs to which Simplify actually produces different
-// counterexamples.
-
-procedure P(x: int)
-{
-start:
-  goto A, B;
-
-A:
-  assert 0 <= x;
-  goto C;
-
-B:
-  assert x < 100;
-  goto C;
-
-C:
-  assert x == 87;
-  return;
-}
+// RUN: %boogie -vc:block -errorLimit:1 -errorTrace:1 -logPrefix:-1block "%s" > "%t1"
+// RUN: %diff "%s.e1.block.expect" "%t1"
+// RUN: %boogie -vc:local -errorLimit:1 -errorTrace:1 -logPrefix:-1local "%s" > "%t2"
+// RUN: %diff "%s.e1.local.expect" "%t2"
+// RUN: %boogie -vc:dag -errorLimit:1 -errorTrace:1 -logPrefix:-1dag "%s" > "%t3"
+// RUN: %diff "%s.e1.dag.expect" "%t3"
+// RUN: %boogie -vc:local -errorLimit:10 -errorTrace:1 -logPrefix:-10local "%s" > "%t4"
+// RUN: %diff "%s.e10.local.expect" "%t4"
+// RUN: %boogie -vc:dag -errorLimit:10 -errorTrace:1 -logPrefix:-10dag "%s" > "%t5"
+// RUN: %diff "%s.e10.dag.expect" "%t5"
+
+// Author of this comment: mikebarnett ec02177eefb5
+// The following tests are rather fickle at the moment--different errors
+// may be reported during different runs.  Moreover, it is conceivable that
+// the error trace would be reported in different orders, since we do not
+// attempt to sort the trace labels at this time.
+// An interesting thing is that /vc:local can with Simplify report more than one
+// error for this file, even with /errorLimit:1.  Other than that, only
+// local and dag produce VCs to which Simplify actually produces different
+// counterexamples.
+
+procedure P(x: int)
+{
+start:
+  goto A, B;
+
+A:
+  assert 0 <= x;
+  goto C;
+
+B:
+  assert x < 100;
+  goto C;
+
+C:
+  assert x == 87;
+  return;
+}
diff --git a/Test/test7/NestedVC.bpl b/Test/test7/NestedVC.bpl
index 6865be93..4fd22d22 100644
--- a/Test/test7/NestedVC.bpl
+++ b/Test/test7/NestedVC.bpl
@@ -1,23 +1,23 @@
-// RUN: %boogie -vc:nested "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure P()
-{
-A: goto B, C;
-B: goto G;
-C: goto D, E;
-D: goto F;
-E: goto F;
-F: goto G;
-G: return;
-}
-
-procedure Q(x: bool)
-{
-A: goto B, C;
-B: assert x; goto G;
-C: goto D, E;
-D: goto F;
-E: goto F;
-F: goto G;
-G: return;
-}
+// RUN: %boogie -vc:nested "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure P()
+{
+A: goto B, C;
+B: goto G;
+C: goto D, E;
+D: goto F;
+E: goto F;
+F: goto G;
+G: return;
+}
+
+procedure Q(x: bool)
+{
+A: goto B, C;
+B: assert x; goto G;
+C: goto D, E;
+D: goto F;
+E: goto F;
+F: goto G;
+G: return;
+}
diff --git a/Test/test7/UnreachableBlocks.bpl b/Test/test7/UnreachableBlocks.bpl
index 95c35029..90f0b0cb 100644
--- a/Test/test7/UnreachableBlocks.bpl
+++ b/Test/test7/UnreachableBlocks.bpl
@@ -1,42 +1,42 @@
-// RUN: %boogie -vc:nested "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// In the following program, block "A" has no dominator, which would cause Boogie
-// to crash if Boogie didn't first remove unreachable blocks.  That is essentially
-// what this test tests
-procedure P()
-{
-entry:
-  goto A;
-A:
-  return;
-B:
-  goto A;
-}
-
-procedure Q()
-{
-entry:
-  goto entry, A;
-A:
-  return;
-}
-
-procedure R()
-{
-entry:
-  return;
-A:
-  goto A;
-}
-
-procedure S()
-{
-entry:
-  return;
-A:
-  goto C;
-B:
-  goto C;
-C:  // C has no dominator
-  return;
-}
+// RUN: %boogie -vc:nested "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// In the following program, block "A" has no dominator, which would cause Boogie
+// to crash if Boogie didn't first remove unreachable blocks.  That is essentially
+// what this test tests
+procedure P()
+{
+entry:
+  goto A;
+A:
+  return;
+B:
+  goto A;
+}
+
+procedure Q()
+{
+entry:
+  goto entry, A;
+A:
+  return;
+}
+
+procedure R()
+{
+entry:
+  return;
+A:
+  goto A;
+}
+
+procedure S()
+{
+entry:
+  return;
+A:
+  goto C;
+B:
+  goto C;
+C:  // C has no dominator
+  return;
+}