summaryrefslogtreecommitdiff
path: root/Test/snapshots/Snapshots2.v2.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/snapshots/Snapshots2.v2.bpl')
-rw-r--r--Test/snapshots/Snapshots2.v2.bpl2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/snapshots/Snapshots2.v2.bpl b/Test/snapshots/Snapshots2.v2.bpl
index 02c5e6df..567191d3 100644
--- a/Test/snapshots/Snapshots2.v2.bpl
+++ b/Test/snapshots/Snapshots2.v2.bpl
@@ -1,7 +1,7 @@
procedure {:checksum "P0$proc#2"} P0();
requires F0();
// Action: verify (procedure changed)
-implementation {:checksum "P0$impl#0"} P0()
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
{
call P0();
}