1 files changed, 163 insertions, 0 deletions
diff --git a/Test/test2/Where.bpl b/Test/test2/Where.bpl
new file mode 100644
index 00000000..96ffcf04
--- /dev/null
+++ b/Test/test2/Where.bpl
@@ -0,0 +1,163 @@
+procedure P0()
+{
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  assert 0 <= x;
+  assert x <= y;
+  assert y < 5;  // error
+}
+
+procedure P1()
+{
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  x := 5;
+  havoc y;
+  assert 5 <= y;
+
+  havoc x;
+  assert 0 <= x;
+  assert x <= y;  // error
+}
+
+procedure P2()
+{
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  havoc y;  // y first
+  havoc x;
+  assert x <= y;  // error
+}
+
+procedure P3()
+{
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  x := 5;
+  havoc x;  // this time, x first
+  havoc y;
+  assert x <= y;  // yeah!
+  assert 5 <= y;  // error
+}
+
+procedure P4()
+{
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  havoc x, y;  // both at the same time
+  assert 0 <= x && x <= y;
+  havoc y, x;  // or in the other order
+  assert 0 <= x && x <= y;
+
+  assert x == 7;  // error
+}
+
+procedure R0() returns (wProc: int where wProc == xProc,
+                        xProc: int where 0 <= xProc,
+                        yProc: int where xProc <= yProc);
+implementation R0() returns (w: int, x: int, y: int)
+{
+  while (*) {
+    assert w == x;
+    assert 0 <= x;
+    assert x <= y;
+  }
+  while (*) {
+    assert w == x;
+    assert 0 <= x;
+    assert x <= y;
+    // the following makes w, x, y loop targets
+    w := w + 1;
+    havoc x;
+    y := w;
+  }
+  assert w == x;
+  assert 0 <= x;
+  assert x <= y;
+}
+
+procedure R1()
+{
+  var a: int;
+  var b: int;
+  var c: int;
+
+  call a, b, c := R0();
+  assert a == b;
+  assert 0 <= b;
+  assert b <= c;
+}
+
+procedure R2()
+{
+  var w: int where w == x;
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  x := 5;
+  y := 10;
+  while (*) {
+    w := w + 1;
+    assert w == 6;
+    y := y + 2;
+    assert 7 <= y;
+  }
+  assert x == 5 && 0 <= y - w;
+  assert y == 10;  // error
+}
+
+procedure R3()
+{
+  var w: int where w == x;
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  // change w and x
+  y := 10;
+  while (*) {
+    w := w;  x := x;
+  }
+  assert w == x;
+  assert 0 <= x;
+  assert y == 10;
+  assert w <= 10;  // error
+}
+
+procedure R4()
+{
+  var w: int where w == x;
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  // change x and y
+  w := 12;
+  while (*) {
+    x := x;  y := y;
+  }
+  assert 0 <= x;
+  assert x <= y;
+  assert w == 12;
+  assert 8 <= y;  // error
+}
+
+procedure R5(K: int)
+{
+  var w: int where w == x;
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  // change w and y
+  x := K;
+  while (*) {
+    w := w;  y := y;
+  }
+  assert w == K;
+  assert K <= y;
+  assert x == K;
+  assert 0 <= x;  // error
+}