1 files changed, 50 insertions, 0 deletions
diff --git a/Test/codeexpr/CodeExpr2.bpl b/Test/codeexpr/CodeExpr2.bpl
new file mode 100644
index 00000000..61758d5a
--- /dev/null
+++ b/Test/codeexpr/CodeExpr2.bpl
@@ -0,0 +1,50 @@
+type T;
+const zero: T;
+
+function IsProperIndex(i: int, size: int): bool;
+
+procedure P(a: [int]T, n: int)
+  requires (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+{
+  call Q(a, n);
+}
+
+procedure Q(a: [int]T, n: int)
+  requires (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+{
+  call P(a, n);
+}
+
+procedure A(a: [int]T, n: int)
+{
+  assert
+    (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero)
+    ==>
+    (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+}
+
+procedure B(a: [int]T, n: int)
+{
+  assert
+    (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|)
+    ==>
+    (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+}
+
+procedure C(a: [int]T, n: int)
+{
+  Start:
+    assume (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+    goto Next;
+  Next:
+    assert (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+}
+
+procedure D(a: [int]T, n: int)
+{
+  Start:
+    assume (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+    goto Next;
+  Next:
+    assert (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+}