Minor change

1 files changed, 100 insertions, 184 deletions

diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect
index e5b3c3d2..474c0b55 100644
--- a/Test/dafny0/snapshots/runtest.snapshot.expect
+++ b/Test/dafny0/snapshots/runtest.snapshot.expect
@@ -1,29 +1,19 @@
 

 -------------------- 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
-

+Processing command (at Snapshots0.v0.dfy(3,3)) 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

+Processing command (at Snapshots0.v0.dfy(4,10)) 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
-

+Processing call to procedure IntraModuleCall$$_module.__default.bar in implementation Impl$$_module.__default.foo (at Snapshots0.v1.dfy(3,3)):

+  >>> 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);

+Processing command (at Snapshots0.v1.dfy(3,3)) 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

+Processing command (at <unknown location>) 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);

+  >>> added assume statement for negation of single assumption variable "a##post##0"

+Processing command (at Snapshots0.v1.dfy(4,10)) 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

@@ -31,33 +21,22 @@ Execution trace:
 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
-

+Processing command (at Snapshots1.v0.dfy(3,3)) 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

+Processing command (at Snapshots1.v0.dfy(4,10)) assert Lit(false) /* checksum: 4E-05-2D-45-F2-42-77-1B-B8-AD-A2-80-42-D8-DB-6C */ ;

+  >>> did nothing

+Processing command (at Snapshots1.v0.dfy(12,3)) 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
-

+Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots1.v1.dfy(3,3)):

+  >>> added after: a##post##0 := a##post##0 && false;

+Processing command (at Snapshots1.v1.dfy(12,3)) assert true /* checksum: BC-E6-1C-AB-CF-AE-26-BF-72-0B-EC-D2-7F-CE-E5-C1 */ ;

+  >>> turned assertion into assume statement

+Processing command (at Snapshots1.v1.dfy(3,3)) 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 */ ;

+  >>> turned assertion into assume statement

+Processing command (at Snapshots1.v1.dfy(4,10)) 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

@@ -65,87 +44,57 @@ Execution trace:
 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
-

+Processing command (at Snapshots2.v0.dfy(3,3)) 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

+Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false) /* checksum: 7A-6A-3E-AD-B0-B1-83-A7-DB-88-34-6C-61-C0-0E-B6 */ ;

+  >>> did nothing

+Processing command (at Snapshots2.v0.dfy(11,11)) assert this == this /* checksum: 9E-07-A8-E4-EB-E7-C7-D8-52-8E-DC-CE-74-A4-B6-6D */ ;

+  >>> did nothing

+Processing command (at Snapshots2.v0.dfy(11,15)) 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

+Processing command (at Snapshots2.v0.dfy(14,11)) assert this == this /* checksum: F6-95-6F-BE-2D-F3-C7-56-EF-72-1F-04-A9-AA-1D-63 */ ;

+  >>> did nothing

+Processing command (at Snapshots2.v0.dfy(14,15)) 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

+Processing command (at Snapshots2.v0.dfy(18,3)) 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
-

+Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots2.v1.dfy(3,3)):

+  >>> added after: a##post##0 := a##post##0 && false;

+Processing command (at Snapshots2.v1.dfy(18,3)) assert true /* checksum: 93-C7-F9-EA-7D-64-8C-C4-DF-34-5F-3A-6A-94-6B-CB */ ;

+  >>> turned assertion into assume statement

+Processing command (at Snapshots2.v1.dfy(3,3)) 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 */ ;

+  >>> turned assertion into assume statement

+Processing command (at Snapshots2.v1.dfy(4,10)) 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
-

+Processing command (at Snapshots2.v1.dfy(11,11)) assert this == this /* checksum: 9E-07-A8-E4-EB-E7-C7-D8-52-8E-DC-CE-74-A4-B6-6D */ ;

+  >>> turned assertion into assume statement

+Processing command (at Snapshots2.v1.dfy(11,15)) 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

+Processing command (at Snapshots2.v1.dfy(14,11)) assert this == this /* checksum: F6-95-6F-BE-2D-F3-C7-56-EF-72-1F-04-A9-AA-1D-63 */ ;

+  >>> turned assertion into assume statement

+Processing command (at Snapshots2.v1.dfy(14,15)) 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
-

+Processing command (at Snapshots3.v0.dfy(9,14)) 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);

+Processing command (at Snapshots3.v1.dfy(5,12)) assert Lit(true) /* checksum: 91-C8-DC-44-53-C2-83-8B-E5-99-59-42-30-2E-D3-E3 */ ;

+  >>> did nothing

+Processing command (at Snapshots3.v1.dfy(9,14)) assert Lit(0 != 0) /* checksum: 72-4B-44-38-EE-E4-82-62-DE-84-D5-C6-FF-FA-4F-FF */ ;

+  >>> recycled error and turned assertion into assume statement

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

 Execution trace:

     (0,0): anon0

@@ -154,23 +103,16 @@ Execution trace:
 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
-

+Processing command (at Snapshots4.v0.dfy(9,14)) 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
-

+Processing command (at Snapshots4.v1.dfy(5,14)) assert Lit(1 != 1) /* checksum: 07-47-65-9A-C5-5D-B0-04-13-66-41-97-34-74-F3-44 */ ;

+  >>> did nothing

+Processing command (at Snapshots4.v1.dfy(9,14)) assert LitInt(0) == LitInt(0) /* checksum: DC-F4-B8-A6-86-FB-52-CE-89-A8-32-46-95-C6-77-44 */ ;

+  >>> turned assertion into assume statement

+Processing command (at Snapshots4.v1.dfy(10,14)) 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

@@ -183,62 +125,40 @@ Execution trace:
 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
-

+Processing command (at Snapshots5.v0.dfy(3,3)) 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

+Processing command (at Snapshots5.v0.dfy(10,40)) 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

+Processing command (at Snapshots5.v0.dfy(12,3)) 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

+Processing command (at Snapshots5.v0.dfy(13,38)) 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

+Processing command (at Snapshots5.v0.dfy(20,40)) 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
-

+Processing command (at Snapshots5.v1.dfy(3,3)) 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 */ ;

+  >>> turned assertion into assume statement

+Processing command (at Snapshots5.v1.dfy(10,40)) 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 */ ;

+  >>> turned assertion into assume statement

+Processing command (at Snapshots5.v1.dfy(12,3)) 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 */ ;

+  >>> turned assertion into assume statement

+Processing command (at Snapshots5.v1.dfy(13,38)) 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 */ ;

+  >>> turned assertion into assume statement

+Processing command (at Snapshots5.v1.dfy(20,40)) 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

+Processing command (at Snapshots5.v1.dfy(22,38)) 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
-

+Processing command (at Snapshots6.v0.dfy(20,14)) 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
-

+Processing command (at Snapshots6.v1.dfy(20,14)) 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

@@ -246,16 +166,12 @@ Execution trace:
 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
-

+Processing command (at Snapshots7.v0.dfy(19,14)) 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
-

+Processing command (at Snapshots7.v1.dfy(19,14)) 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