From 91a0cf94be3cdfaff29d65122c9ea031a1a4976b Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Fri, 12 Feb 2016 15:59:08 -0800
Subject: Fix issue 132. The formal argument can't be assume to be allocated
 when a function is invoked inside an "Old" expression.

---
 Test/dafny4/Bug132.dfy.expect | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 Test/dafny4/Bug132.dfy.expect

(limited to 'Test/dafny4/Bug132.dfy.expect')

diff --git a/Test/dafny4/Bug132.dfy.expect b/Test/dafny4/Bug132.dfy.expect
new file mode 100644
index 00000000..0452f42d
--- /dev/null
+++ b/Test/dafny4/Bug132.dfy.expect
@@ -0,0 +1,18 @@
+Bug132.dfy(33,29): Error: receiver argument must be allocated in the state in which the function is invoked
+Execution trace:
+    (0,0): anon0
+    (0,0): anon24_Then
+Bug132.dfy(34,29): Error: receiver argument must be allocated in the state in which the function is invoked
+Execution trace:
+    (0,0): anon0
+    (0,0): anon25_Then
+Bug132.dfy(37,36): Error: argument must be allocated in the state in which the function is invoked
+Execution trace:
+    (0,0): anon0
+    (0,0): anon26_Then
+Bug132.dfy(41,29): Error: receiver argument must be allocated in the state in which the function is invoked
+Execution trace:
+    (0,0): anon0
+    (0,0): anon27_Then
+
+Dafny program verifier finished with 3 verified, 4 errors
-- 
cgit v1.2.3