From a16ac98f4aa7657d999753e299e32613e10f1c5d Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Fri, 2 Dec 2011 10:58:47 +0100
Subject: Boogie: Fixed a crash due to old expressions in lambda expressions
 that were not replaced after lambda expansion.

(reported by Florian Egli)
---
 Test/test2/LambdaOldExpressions.bpl | 39 +++++++++++++++++++++++++++++++++++++
 Test/test2/runtest.bat              |  3 ++-
 2 files changed, 41 insertions(+), 1 deletion(-)
 create mode 100644 Test/test2/LambdaOldExpressions.bpl

(limited to 'Test/test2')

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];
+}
diff --git a/Test/test2/runtest.bat b/Test/test2/runtest.bat
index 8ce2f66e..f32bf844 100644
--- a/Test/test2/runtest.bat
+++ b/Test/test2/runtest.bat
@@ -11,7 +11,8 @@ for %%f in (FormulaTerm.bpl FormulaTerm2.bpl Passification.bpl B.bpl
             strings-no-where.bpl strings-where.bpl
             Structured.bpl Where.bpl UpdateExpr.bpl
             NeverPattern.bpl NullaryMaps.bpl Implies.bpl
-            IfThenElse1.bpl Lambda.bpl LambdaPoly.bpl SelectiveChecking.bpl FreeCall.bpl) do (
+            IfThenElse1.bpl Lambda.bpl LambdaPoly.bpl LambdaOldExpressions.bpl
+            SelectiveChecking.bpl FreeCall.bpl) do (
   echo.
   echo -------------------- %%f --------------------
   %BGEXE% %* /noinfer %%f
-- 
cgit v1.2.3