From 0658816bbe2ea4be8785b52958a65b55c6a845a5 Mon Sep 17 00:00:00 2001
From: Valentin Wüstholz <wuestholz@gmail.com>
Date: Fri, 12 Jun 2015 01:26:06 +0200
Subject: Add a test case.

---
 Test/snapshots/Snapshots36.v0.bpl      | 14 ++++++++++++++
 Test/snapshots/Snapshots36.v1.bpl      | 14 ++++++++++++++
 Test/snapshots/runtest.snapshot        |  2 +-
 Test/snapshots/runtest.snapshot.expect |  9 +++++++++
 4 files changed, 38 insertions(+), 1 deletion(-)
 create mode 100644 Test/snapshots/Snapshots36.v0.bpl
 create mode 100644 Test/snapshots/Snapshots36.v1.bpl

(limited to 'Test/snapshots')

diff --git a/Test/snapshots/Snapshots36.v0.bpl b/Test/snapshots/Snapshots36.v0.bpl
new file mode 100644
index 00000000..9417af97
--- /dev/null
+++ b/Test/snapshots/Snapshots36.v0.bpl
@@ -0,0 +1,14 @@
+function {:checksum "2"} F() : bool
+{
+    true
+}
+
+procedure {:checksum "0"} P(b: bool);
+
+implementation {:id "P"} {:checksum "1"} P(p: bool)
+{
+    var l: [int]bool;
+
+    l := (lambda n: int :: F());
+    assert l[0];
+}
diff --git a/Test/snapshots/Snapshots36.v1.bpl b/Test/snapshots/Snapshots36.v1.bpl
new file mode 100644
index 00000000..317182a5
--- /dev/null
+++ b/Test/snapshots/Snapshots36.v1.bpl
@@ -0,0 +1,14 @@
+function {:checksum "3"} F() : bool
+{
+    false
+}
+
+procedure {:checksum "0"} P(b: bool);
+
+implementation {:id "P"} {:checksum "1"} P(p: bool)
+{
+    var l: [int]bool;
+
+    l := (lambda n: int :: F());
+    assert l[0];
+}
diff --git a/Test/snapshots/runtest.snapshot b/Test/snapshots/runtest.snapshot
index 01a231fe..608ac2d2 100644
--- a/Test/snapshots/runtest.snapshot
+++ b/Test/snapshots/runtest.snapshot
@@ -1,2 +1,2 @@
-// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl Snapshots34.bpl Snapshots35.bpl > "%t"
+// RUN: %boogie -errorTrace:0 -traceCaching:1 -verifySnapshots:2 -verifySeparately -noinfer Snapshots0.bpl Snapshots1.bpl Snapshots2.bpl Snapshots3.bpl Snapshots4.bpl Snapshots5.bpl Snapshots6.bpl Snapshots7.bpl Snapshots8.bpl Snapshots9.bpl Snapshots10.bpl Snapshots11.bpl Snapshots12.bpl Snapshots13.bpl Snapshots14.bpl Snapshots15.bpl Snapshots16.bpl Snapshots17.bpl Snapshots18.bpl Snapshots19.bpl Snapshots20.bpl Snapshots21.bpl Snapshots22.bpl Snapshots23.bpl Snapshots24.bpl Snapshots25.bpl Snapshots26.bpl Snapshots27.bpl Snapshots28.bpl Snapshots30.bpl Snapshots31.bpl Snapshots32.bpl Snapshots33.bpl Snapshots34.bpl Snapshots35.bpl Snapshots36.bpl > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index 637dd088..44ed6a3b 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -648,3 +648,12 @@ Processing command (at Snapshots35.v1.bpl(5,5)) assert p;
 Snapshots35.v1.bpl(5,5): Error BP5001: This assertion might not hold.
 
 Boogie program verifier finished with 0 verified, 1 error
+Processing command (at Snapshots36.v0.bpl(13,5)) assert l[0];
+  >>> DoNothingToAssert
+
+Boogie program verifier finished with 1 verified, 0 errors
+Processing command (at Snapshots36.v1.bpl(13,5)) assert l[0];
+  >>> DoNothingToAssert
+Snapshots36.v1.bpl(13,5): Error BP5001: This assertion might not hold.
+
+Boogie program verifier finished with 0 verified, 1 error
-- 
cgit v1.2.3