Make the dependency analysis for snapshot verification take 'where' clauses into account.

1 files changed, 4 insertions, 4 deletions

diff --git a/Test/snapshots/Snapshots4.v1.bpl b/Test/snapshots/Snapshots4.v1.bpl
index 025a3f5f..392a1648 100644
--- a/Test/snapshots/Snapshots4.v1.bpl
+++ b/Test/snapshots/Snapshots4.v1.bpl
@@ -1,7 +1,7 @@
 procedure {:checksum "P0$proc#0"} P0();

 // Action: skip

 // Priority: 0

-implementation {:checksum "P0$impl#0"} P0()

+implementation {:id "P0"} {:checksum "P0$impl#0"} P0()

 {

 }

 

@@ -9,7 +9,7 @@ implementation {:checksum "P0$impl#0"} P0()
 procedure {:checksum "P1$proc#0"} P1();

 // Action: verify

 // Priority: 1

-implementation {:checksum "P1$impl#0"} P1()

+implementation {:id "P1"} {:checksum "P1$impl#0"} P1()

 {

     call P2();

 }

@@ -18,7 +18,7 @@ implementation {:checksum "P1$impl#0"} P1()
 procedure {:checksum "P3$proc#0"} P3();

 // Action: verify

 // Priority: 2

-implementation {:checksum "P3$impl#1"} P3()

+implementation {:id "P3"} {:checksum "P3$impl#1"} P3()

 {

     assert false;

 }

@@ -28,7 +28,7 @@ procedure {:checksum "P2$proc#0"} P2();
   ensures G();

 // Action: verify

 // Priority: 3

-implementation {:checksum "P2$impl#0"} P2()

+implementation {:id "P2"} {:checksum "P2$impl#0"} P2()

 {

 }