summaryrefslogtreecommitdiff
path: root/Test/snapshots/Snapshots15.v0.bpl
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2014-06-26 23:57:21 +0200
committerGravatar wuestholz <unknown>2014-06-26 23:57:21 +0200
commitd7a66f4944c89ac82e7389cf18b7ecffc94e31f0 (patch)
treed9ea80ede2f275d5e2473fcadb4a3ac07382e256 /Test/snapshots/Snapshots15.v0.bpl
parentf2742460f1fe65bde86dd30b0c8523b1eea40a4f (diff)
Optimized the way that assertions are marked as partially verified.
Diffstat (limited to 'Test/snapshots/Snapshots15.v0.bpl')
-rw-r--r--Test/snapshots/Snapshots15.v0.bpl4
1 files changed, 4 insertions, 0 deletions
diff --git a/Test/snapshots/Snapshots15.v0.bpl b/Test/snapshots/Snapshots15.v0.bpl
index 3dbf492e..a947157d 100644
--- a/Test/snapshots/Snapshots15.v0.bpl
+++ b/Test/snapshots/Snapshots15.v0.bpl
@@ -2,8 +2,12 @@ procedure {:checksum "0"} M();
implementation {:id "M"} {:checksum "1"} M()
{
+ assert true;
+
call N();
+ assert true;
+
call N();
assert false;