Boogie: Fixed a crash due to old expressions in lambda expressions that were not replaced after lambda expansion.

(reported by Florian Egli)

1 files changed, 39 insertions, 0 deletions

diff --git a/Test/test2/LambdaOldExpressions.bpl b/Test/test2/LambdaOldExpressions.bpl
new file mode 100644
index 00000000..c26b0198
--- /dev/null
+++ b/Test/test2/LambdaOldExpressions.bpl
@@ -0,0 +1,39 @@
+var b: bool;

+

+

+procedure p0();

+  requires b;

+  modifies b;

+  ensures (lambda x: bool :: old(b))[true];

+  ensures !(lambda x: bool :: b)[true];

+

+implementation p0()

+{

+    b := !b;

+    assert (lambda x: bool :: old(b))[true];

+    assert !(lambda x: bool :: b)[true];

+}

+

+

+procedure p1();

+  requires !b;

+  modifies b;

+  ensures (lambda x: bool :: old(b))[true];  // error

+

+implementation p1()

+{

+    b := !b;

+    assert !(lambda x: bool :: old(b))[true];

+}

+

+

+procedure p2();

+  requires b;

+  modifies b;

+  ensures (lambda x: bool :: old(b) != b)[true];

+

+implementation p2()

+{

+    b := !b;

+    assert (lambda x: bool :: old(b) != b)[true];

+}