1 files changed, 86 insertions, 0 deletions
diff --git a/Test/test2/B.bpl b/Test/test2/B.bpl
new file mode 100644
index 00000000..553d5002
--- /dev/null
+++ b/Test/test2/B.bpl
@@ -0,0 +1,86 @@
+// ----------- BEGIN PRELUDE
+
+var Heap: [ref, name]int;
+const N: name;
+
+procedure Q0()
+{
+  var h: int;
+
+  entry:
+    goto Else;
+
+  Then:
+    h := 15;
+    goto end;
+
+  Else:
+    assume h == 0;
+    goto end;
+
+  end:
+    assert 0 <= h;
+    return;
+}
+
+procedure Q1()
+{
+  var h: int;
+
+  entry:
+    goto Else;
+
+  Then:
+    h := -15;
+    goto end;
+
+  Else:
+    assume h == 0;
+    goto end;
+
+  end:
+    h := -h;
+    assert 0 <= h;
+    return;
+}
+
+procedure P0(this: ref)
+  modifies Heap;
+{
+  entry:
+    goto Else;
+
+  Then:
+    Heap[this, N] := 15;
+    goto end;
+
+  Else:
+    assume Heap[this, N] == 0;
+    goto end;
+
+  end:
+    assert 0 <= Heap[this, N];
+    return;
+}
+
+procedure P1(this: ref)
+  modifies Heap;
+{
+  entry:
+    goto Else;
+
+  Then:
+    Heap[this, N] := -15;
+    goto end;
+
+  Else:
+    assume Heap[this, N] == 0;
+    goto end;
+
+  end:
+    Heap[this, N] := -Heap[this, N];
+    assert 0 <= Heap[this, N];
+    return;
+}
+
+type name, ref;