Made it use the '/traceCaching' flag for the 'snapshots' tests.

2 files changed, 185 insertions, 1 deletions

diff --git a/Test/dafny0/snapshots/runtest.snapshot b/Test/dafny0/snapshots/runtest.snapshot
index 8bf5b22f..62ccabb3 100644
--- a/Test/dafny0/snapshots/runtest.snapshot
+++ b/Test/dafny0/snapshots/runtest.snapshot
@@ -1,2 +1,2 @@
-// RUN: %dafny /compile:0 /verifySnapshots:2 /verifySeparately Snapshots0.dfy Snapshots1.dfy Snapshots2.dfy Snapshots3.dfy Snapshots4.dfy Snapshots5.dfy Snapshots6.dfy Snapshots7.dfy  > "%t"
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 /verifySeparately Snapshots0.dfy Snapshots1.dfy Snapshots2.dfy Snapshots3.dfy Snapshots4.dfy Snapshots5.dfy Snapshots6.dfy Snapshots7.dfy  > "%t"
 // RUN: %diff "%s.expect" "%t"
diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect
index 5dfa1d86..e5b3c3d2 100644
--- a/Test/dafny0/snapshots/runtest.snapshot.expect
+++ b/Test/dafny0/snapshots/runtest.snapshot.expect
@@ -1,7 +1,29 @@
 

 -------------------- Snapshots0.dfy --------------------

 

+assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]) /* checksum: A0-B4-50-60-9F-FE-44-6C-9C-B7-4F-16-C3-B5-03-42 */ ;

+==> did nothing
+

+

+assert Lit(false) /* checksum: 39-6A-22-AE-E4-77-C0-68-32-5F-2A-F1-4C-3E-3A-21 */ ;

+==> did nothing
+

+

 Dafny program verifier finished with 3 verified, 0 errors

+
+For call to IntraModuleCall$$_module.__default.bar in Impl$$_module.__default.foo:

++ Added after: a##post##0 := a##post##0 && true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call1old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call1old#AT#$Heap, $o, $f)) && $HeapSucc(call1old#AT#$Heap, $Heap);

+

+assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]) /* checksum: A0-B4-50-60-9F-FE-44-6C-9C-B7-4F-16-C3-B5-03-42 */ ;

+==> did nothing
+

+

+a##post##0 := a##post##0 && true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call1old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call1old#AT#$Heap, $o, $f)) && $HeapSucc(call1old#AT#$Heap, $Heap);

+== assumed negation of single assumption variable ==> assume !a##post##0#AT#0;

+

+assert Lit(false) /* checksum: 39-6A-22-AE-E4-77-C0-68-32-5F-2A-F1-4C-3E-3A-21 */ ;

+==> did nothing
+

 Snapshots0.v1.dfy(4,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

@@ -10,7 +32,32 @@ Dafny program verifier finished with 2 verified, 1 error
 

 -------------------- Snapshots1.dfy --------------------

 

+assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]) /* checksum: BA-71-5B-3A-6A-84-35-ED-7D-74-F2-82-4F-82-B9-43 */ ;

+==> did nothing
+

+

+assert Lit(false) /* checksum: 4E-05-2D-45-F2-42-77-1B-B8-AD-A2-80-42-D8-DB-6C */ ;

+==> did nothing
+

+

+assert true /* checksum: BC-E6-1C-AB-CF-AE-26-BF-72-0B-EC-D2-7F-CE-E5-C1 */ ;

+==> did nothing
+

+

 Dafny program verifier finished with 4 verified, 0 errors

+
+For call to IntraModuleCall$$_module.__default.N in Impl$$_module.__default.M:

++ Added after: a##post##0 := a##post##0 && false;

+

+assert true /* checksum: BC-E6-1C-AB-CF-AE-26-BF-72-0B-EC-D2-7F-CE-E5-C1 */ ;

+== marked as fully verified ==> assume {:verified_assertion} true;

+

+assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]) /* checksum: BA-71-5B-3A-6A-84-35-ED-7D-74-F2-82-4F-82-B9-43 */ ;

+== marked as fully verified ==> assume {:verified_assertion} (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame#AT#0[$o, $f]);

+

+assert Lit(false) /* checksum: 4E-05-2D-45-F2-42-77-1B-B8-AD-A2-80-42-D8-DB-6C */ ;

+==> did nothing
+

 Snapshots1.v1.dfy(4,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

@@ -19,20 +66,86 @@ Dafny program verifier finished with 3 verified, 1 error
 

 -------------------- Snapshots2.dfy --------------------

 

+assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]) /* checksum: 46-E2-58-52-A8-7B-09-D1-12-29-20-6E-F0-9A-64-05 */ ;

+==> did nothing
+

+

+assert Lit(false) /* checksum: 7A-6A-3E-AD-B0-B1-83-A7-DB-88-34-6C-61-C0-0E-B6 */ ;

+==> did nothing
+

+

+assert this == this /* checksum: 9E-07-A8-E4-EB-E7-C7-D8-52-8E-DC-CE-74-A4-B6-6D */ ;

+==> did nothing
+

+

+assert Lit(_module.__default.P($LS($LS($LZ)), $Heap, this)) <==> Lit(_module.__default.Q($LS($LS($LZ)), $Heap, this)) /* checksum: 41-84-DB-6E-52-33-FA-65-83-01-01-04-53-4E-DC-F7 */ ;

+==> did nothing
+

+

+assert this == this /* checksum: F6-95-6F-BE-2D-F3-C7-56-EF-72-1F-04-A9-AA-1D-63 */ ;

+==> did nothing
+

+

+assert Lit(_module.__default.Q($LS($LS($LZ)), $Heap, this)) <==> Lit(_module.__default.R($Heap, this)) /* checksum: 70-C2-C7-02-D7-99-8D-47-F1-B1-DF-23-5B-1B-29-EC */ ;

+==> did nothing
+

+

+assert true /* checksum: 93-C7-F9-EA-7D-64-8C-C4-DF-34-5F-3A-6A-94-6B-CB */ ;

+==> did nothing
+

+

 Dafny program verifier finished with 6 verified, 0 errors

+
+For call to IntraModuleCall$$_module.__default.N in Impl$$_module.__default.M:

++ Added after: a##post##0 := a##post##0 && false;

+

+assert true /* checksum: 93-C7-F9-EA-7D-64-8C-C4-DF-34-5F-3A-6A-94-6B-CB */ ;

+== marked as fully verified ==> assume {:verified_assertion} true;

+

+assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]) /* checksum: 46-E2-58-52-A8-7B-09-D1-12-29-20-6E-F0-9A-64-05 */ ;

+== marked as fully verified ==> assume {:verified_assertion} (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame#AT#0[$o, $f]);

+

+assert Lit(false) /* checksum: 7A-6A-3E-AD-B0-B1-83-A7-DB-88-34-6C-61-C0-0E-B6 */ ;

+==> did nothing
+

 Snapshots2.v1.dfy(4,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

+assert this == this /* checksum: 9E-07-A8-E4-EB-E7-C7-D8-52-8E-DC-CE-74-A4-B6-6D */ ;

+== marked as fully verified ==> assume {:verified_assertion} this == this;

+

+assert Lit(_module.__default.P($LS($LS($LZ)), $Heap, this)) <==> Lit(_module.__default.Q($LS($LS($LZ)), $Heap, this)) /* checksum: 7D-F5-78-F9-4E-21-45-C8-01-3D-4B-EF-96-1A-40-84 */ ;

+==> did nothing
+

+

+assert this == this /* checksum: F6-95-6F-BE-2D-F3-C7-56-EF-72-1F-04-A9-AA-1D-63 */ ;

+== marked as fully verified ==> assume {:verified_assertion} this == this;

+

+assert Lit(_module.__default.Q($LS($LS($LZ)), $Heap, this)) <==> Lit(_module.__default.R($Heap, this)) /* checksum: EB-D2-14-5B-9A-60-EB-69-91-FB-F8-18-CA-DC-F3-8D */ ;

+==> did nothing
+

+

 Dafny program verifier finished with 5 verified, 1 error

 

 -------------------- Snapshots3.dfy --------------------

+

+assert Lit(0 != 0) /* checksum: 72-4B-44-38-EE-E4-82-62-DE-84-D5-C6-FF-FA-4F-FF */ ;

+==> did nothing
+

 Snapshots3.v0.dfy(9,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

 

 Dafny program verifier finished with 1 verified, 1 error

+

+assert Lit(true) /* checksum: 91-C8-DC-44-53-C2-83-8B-E5-99-59-42-30-2E-D3-E3 */ ;

+==> did nothing
+

+

+assert Lit(0 != 0) /* checksum: 72-4B-44-38-EE-E4-82-62-DE-84-D5-C6-FF-FA-4F-FF */ ;

+== recycled error ==> assume {:recycled_failing_assertion} Lit(0 != 0);

 Snapshots3.v0.dfy(9,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

@@ -42,7 +155,22 @@ Dafny program verifier finished with 1 verified, 1 error
 

 -------------------- Snapshots4.dfy --------------------

 

+assert LitInt(0) == LitInt(0) /* checksum: DC-F4-B8-A6-86-FB-52-CE-89-A8-32-46-95-C6-77-44 */ ;

+==> did nothing
+

+

 Dafny program verifier finished with 2 verified, 0 errors

+

+assert Lit(1 != 1) /* checksum: 07-47-65-9A-C5-5D-B0-04-13-66-41-97-34-74-F3-44 */ ;

+==> did nothing
+

+

+assert LitInt(0) == LitInt(0) /* checksum: DC-F4-B8-A6-86-FB-52-CE-89-A8-32-46-95-C6-77-44 */ ;

+== marked as fully verified ==> assume {:verified_assertion} LitInt(0) == LitInt(0);

+

+assert Lit(2 != 2) /* checksum: 2D-1B-77-03-5D-96-34-D8-29-21-07-0B-78-2F-E9-DB */ ;

+==> did nothing
+

 Snapshots4.v1.dfy(5,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

@@ -56,13 +184,61 @@ Dafny program verifier finished with 1 verified, 2 errors
 

 -------------------- Snapshots5.dfy --------------------

 

+assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]) /* checksum: A0-B4-50-60-9F-FE-44-6C-9C-B7-4F-16-C3-B5-03-42 */ ;

+==> did nothing
+

+

+assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0 /* checksum: F5-C2-A4-FA-E3-68-61-B0-9E-67-CF-D6-EB-82-4B-83 */ ;

+==> did nothing
+

+

+assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]) /* checksum: 52-12-87-8B-4B-EC-C8-CE-B0-B1-32-B7-07-89-DA-63 */ ;

+==> did nothing
+

+

+assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3 /* checksum: 01-BD-3B-F5-9F-4C-6E-A4-02-18-DC-91-9D-9B-D2-38 */ ;

+==> did nothing
+

+

+assert (forall b#5: bool :: true ==> b#5 || !b#5) || 1 != 1 /* checksum: 23-47-65-F9-36-74-DB-E0-DA-7C-DC-98-35-95-54-0F */ ;

+==> did nothing
+

+

 Dafny program verifier finished with 3 verified, 0 errors

 

+assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]) /* checksum: A0-B4-50-60-9F-FE-44-6C-9C-B7-4F-16-C3-B5-03-42 */ ;

+== marked as fully verified ==> assume {:verified_assertion} (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame#AT#0[$o, $f]);

+

+assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0 /* checksum: F5-C2-A4-FA-E3-68-61-B0-9E-67-CF-D6-EB-82-4B-83 */ ;

+== marked as fully verified ==> assume {:verified_assertion} (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;

+

+assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]) /* checksum: 52-12-87-8B-4B-EC-C8-CE-B0-B1-32-B7-07-89-DA-63 */ ;

+== marked as fully verified ==> assume {:verified_assertion} (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame#AT#0[$o, $f]);

+

+assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3 /* checksum: 01-BD-3B-F5-9F-4C-6E-A4-02-18-DC-91-9D-9B-D2-38 */ ;

+== marked as fully verified ==> assume {:verified_assertion} (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;

+

+assert (exists b#5: bool :: b#5 || !b#5) || 4 != 4 /* checksum: 0A-7D-56-D6-BD-AD-1D-7A-48-E5-4E-0E-FD-83-27-25 */ ;

+==> did nothing
+

+

+assert (exists b#7: bool :: b#7 || !b#7) || 5 != 5 /* checksum: 0F-FC-46-D6-72-EB-6E-10-B7-34-F6-DC-A8-99-A8-0B */ ;

+==> did nothing
+

+

 Dafny program verifier finished with 3 verified, 0 errors

 

 -------------------- Snapshots6.dfy --------------------

 

+assert Lit(false) /* checksum: A6-5F-6D-B7-60-AB-45-CE-4C-FD-E0-69-E7-7E-05-E3 */ ;

+==> did nothing
+

+

 Dafny program verifier finished with 4 verified, 0 errors

+

+assert Lit(false) /* checksum: EA-3F-28-16-79-D1-07-91-F8-94-CC-E2-F0-23-6C-CB */ ;

+==> did nothing
+

 Snapshots6.v1.dfy(20,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

@@ -71,7 +247,15 @@ Dafny program verifier finished with 3 verified, 1 error
 

 -------------------- Snapshots7.dfy --------------------

 

+assert Lit(false) /* checksum: 8F-C4-55-DD-29-80-5A-2A-14-A2-21-C0-FD-B5-84-08 */ ;

+==> did nothing
+

+

 Dafny program verifier finished with 4 verified, 0 errors

+

+assert Lit(false) /* checksum: B3-E4-22-86-3E-12-E4-67-20-A1-05-65-FC-4E-CB-E0 */ ;

+==> did nothing
+

 Snapshots7.v1.dfy(19,14): Error: assertion violation

 Execution trace:

     (0,0): anon0