From 75542ea0ee9f14ef18eee6e3349747a8f7181b51 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 10 Nov 2014 10:48:12 +0100
Subject: Worked on the verification result caching.

---
 Test/snapshots/runtest.snapshot.expect | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'Test')

diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index cf588e65..f34fefbe 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -203,7 +203,7 @@ Boogie program verifier finished with 0 verified, 1 error
 Processing call to procedure N in implementation M (at Snapshots11.v1.bpl(7,5)):
   >>> added before precondition check: assume {:precondition_previous_snapshot} 0 < call0formal#AT#n;
   >>> added after: a##post##0 := a##post##0 && 0 < call1formal#AT#r;
-Processing command (at Snapshots11.v1.bpl(7,5)) assume {:precondition_previous_snapshot} 0 < n;
+Processing command (at Snapshots11.v1.bpl(7,5)) assume {:precondition_previous_snapshot} 0 < call0formal#AT#n;
   >>> DropAssume
 Processing command (at Snapshots11.v1.bpl(7,5)) assert 0 < call0formal#AT#n;
   >>> RecycleError
@@ -450,6 +450,8 @@ Processing command (at Snapshots24.v1.bpl(11,9)) assert {:subsumption 1} 5 == 5;
   >>> DoNothingToAssert
 Processing command (at Snapshots24.v1.bpl(15,9)) assert {:subsumption 2} 6 != 6;
   >>> RecycleError
+Processing command (at Snapshots24.v1.bpl(19,9)) assert {:subsumption 1} 2 == 2;
+  >>> DoNothingToAssert
 Processing command (at Snapshots24.v1.bpl(20,9)) assert {:subsumption 2} 4 == 4;
   >>> MarkAsFullyVerified
 Processing command (at Snapshots24.v1.bpl(21,9)) assert 5 == 5;
-- 
cgit v1.2.3