summaryrefslogtreecommitdiff
path: root/Test/snapshots/Snapshots3.v1.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/snapshots/Snapshots3.v1.bpl')
-rw-r--r--Test/snapshots/Snapshots3.v1.bpl2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/snapshots/Snapshots3.v1.bpl b/Test/snapshots/Snapshots3.v1.bpl
index 329382ac..5eb57e78 100644
--- a/Test/snapshots/Snapshots3.v1.bpl
+++ b/Test/snapshots/Snapshots3.v1.bpl
@@ -1,7 +1,7 @@
procedure {:checksum "P0$proc#0"} P0();
ensures G();
// Action: verify
-implementation {:checksum "P0$impl#0"} P0()
+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()
{
}