From 039629ed61cd9537a7b99e0e2993d8d641d79d76 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Sun, 19 Oct 2014 19:39:35 +0200
Subject: Worked on the verification result caching.

---
 Test/snapshots/Snapshots28.v1.bpl      |  2 +-
 Test/snapshots/runtest.snapshot.expect | 11 ++++++-----
 2 files changed, 7 insertions(+), 6 deletions(-)

(limited to 'Test/snapshots')

diff --git a/Test/snapshots/Snapshots28.v1.bpl b/Test/snapshots/Snapshots28.v1.bpl
index 881fa496..0312b6a6 100644
--- a/Test/snapshots/Snapshots28.v1.bpl
+++ b/Test/snapshots/Snapshots28.v1.bpl
@@ -12,5 +12,5 @@ implementation {:id "M"} {:checksum "2"} M()
     }
 
     assert 0 == 0;
-    assert x == 0;  // TODO(wuestholz): This should fail.
+    assert x == 0;
 }
diff --git a/Test/snapshots/runtest.snapshot.expect b/Test/snapshots/runtest.snapshot.expect
index 3b47d2f3..e2355cd6 100644
--- a/Test/snapshots/runtest.snapshot.expect
+++ b/Test/snapshots/runtest.snapshot.expect
@@ -507,9 +507,10 @@ Processing command (at Snapshots28.v0.bpl(14,5)) assert x == 0 /* checksum: 01-A
   >>> did nothing
 
 Boogie program verifier finished with 1 verified, 0 errors
-Processing command (at Snapshots28.v1.bpl(14,5)) assert 0 == 0 /* checksum: AB-78-39-B7-C9-1E-4B-24-B5-1A-52-BE-B2-1A-90-D9 */ ;
-  >>> turned assertion into assume statement
-Processing command (at Snapshots28.v1.bpl(15,5)) assert x == 0 /* checksum: 01-A7-D9-2B-A8-C4-4F-BB-44-22-BE-B6-E1-5F-6E-BF */ ;
-  >>> turned assertion into assume statement
+Processing command (at Snapshots28.v1.bpl(14,5)) assert 0 == 0 /* checksum: B7-69-FE-C9-83-D5-67-99-AA-4C-CE-F9-C4-21-A6-3E */ ;
+  >>> did nothing
+Processing command (at Snapshots28.v1.bpl(15,5)) assert x == 0 /* checksum: 9D-98-FC-55-22-AD-23-60-39-30-A2-93-D3-86-04-7A */ ;
+  >>> did nothing
+Snapshots28.v1.bpl(15,5): Error BP5001: This assertion might not hold.
 
-Boogie program verifier finished with 1 verified, 0 errors
+Boogie program verifier finished with 0 verified, 1 error
-- 
cgit v1.2.3