Merge

2 files changed, 48 insertions, 48 deletions

diff --git a/Test/dafny0/DirtyLoops.dfy b/Test/dafny0/DirtyLoops.dfy
index 5d356f0a..d3164fa9 100644
--- a/Test/dafny0/DirtyLoops.dfy
+++ b/Test/dafny0/DirtyLoops.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:0 "%t.dprint.dfy" >> "%t"

+// RUN: %dafny /compile:0 /dprint:"%t.dprint.dfy" "%s" > "%t"; %dafny /noVerify /compile:1 "%t.dprint.dfy" >> "%t"

 // RUN: %diff "%s.expect" "%t"

 

 method M0(S: set<int>) {

diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect
index 75f0b28f..47cb6952 100644
--- a/Test/dafny0/snapshots/runtest.snapshot.expect
+++ b/Test/dafny0/snapshots/runtest.snapshot.expect
@@ -1,19 +1,19 @@
 

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

 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

+  >>> DoNothingToAssert

 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

+  >>> DoNothingToAssert

 

 Dafny program verifier finished with 3 verified, 0 errors

 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

+  >>> MarkAsFullyVerified

 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"

+  >>> AssumeNegationOfAssumptionVariable

 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

+  >>> MarkAsPartiallyVerified

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

 Execution trace:

     (0,0): anon0

@@ -22,21 +22,21 @@ Dafny program verifier finished with 2 verified, 1 error
 

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

 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

+  >>> DoNothingToAssert

 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

+  >>> DoNothingToAssert

 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

+  >>> DoNothingToAssert

 

 Dafny program verifier finished with 4 verified, 0 errors

 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

+  >>> MarkAsFullyVerified

 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

+  >>> MarkAsFullyVerified

 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

+  >>> DoNothingToAssert

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

 Execution trace:

     (0,0): anon0

@@ -45,46 +45,46 @@ Dafny program verifier finished with 3 verified, 1 error
 

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

 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

+  >>> DoNothingToAssert

 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

+  >>> DoNothingToAssert

 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

+  >>> DoNothingToAssert

 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

+  >>> DoNothingToAssert

 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

+  >>> DoNothingToAssert

 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

+  >>> DoNothingToAssert

 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

+  >>> DoNothingToAssert

 

 Dafny program verifier finished with 6 verified, 0 errors

 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

+  >>> MarkAsFullyVerified

 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

+  >>> MarkAsFullyVerified

 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

+  >>> DoNothingToAssert

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

 Execution trace:

     (0,0): anon0

 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

+  >>> MarkAsFullyVerified

 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

+  >>> DoNothingToAssert

 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

+  >>> MarkAsFullyVerified

 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

+  >>> DoNothingToAssert

 

 Dafny program verifier finished with 5 verified, 1 error

 

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

 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

+  >>> DoNothingToAssert

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

 Execution trace:

     (0,0): anon0

@@ -92,9 +92,9 @@ Execution trace:
 

 Dafny program verifier finished with 1 verified, 1 error

 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

+  >>> DoNothingToAssert

 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

+  >>> RecycleError

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

 Execution trace:

     (0,0): anon0

@@ -104,15 +104,15 @@ Dafny program verifier finished with 1 verified, 1 error
 

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

 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

+  >>> DoNothingToAssert

 

 Dafny program verifier finished with 2 verified, 0 errors

 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

+  >>> DoNothingToAssert

 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

+  >>> MarkAsFullyVerified

 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

+  >>> DoNothingToAssert

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

 Execution trace:

     (0,0): anon0

@@ -126,39 +126,39 @@ Dafny program verifier finished with 1 verified, 2 errors
 

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

 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

+  >>> DoNothingToAssert

 Processing command (at Snapshots5.v0.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0 /* checksum: F5-42-1C-46-53-48-B1-C8-9E-E7-CF-D6-6B-C2-33-83 */ ;

-  >>> did nothing

+  >>> DoNothingToAssert

 Processing command (at Snapshots5.v0.dfy(12,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]) /* checksum: 52-92-0F-5F-BB-CC-18-D6-B0-31-32-B7-87-C9-F2-63 */ ;

-  >>> did nothing

+  >>> DoNothingToAssert

 Processing command (at Snapshots5.v0.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3 /* checksum: 01-09-3B-C5-5F-C0-D6-24-82-98-EC-A1-9D-9B-D2-38 */ ;

-  >>> did nothing

+  >>> DoNothingToAssert

 Processing command (at Snapshots5.v0.dfy(20,40)) assert (forall b#5: bool :: true ==> b#5 || !b#5) || 1 != 1 /* checksum: A3-47-65-A9-36-74-DB-60-BE-7C-DC-78-B5-15-54-0F */ ;

-  >>> did nothing

+  >>> DoNothingToAssert

 

 Dafny program verifier finished with 3 verified, 0 errors

 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

+  >>> MarkAsFullyVerified

 Processing command (at Snapshots5.v1.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0 /* checksum: F5-42-1C-46-53-48-B1-C8-9E-E7-CF-D6-6B-C2-33-83 */ ;

-  >>> turned assertion into assume statement

+  >>> MarkAsFullyVerified

 Processing command (at Snapshots5.v1.dfy(12,3)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]) /* checksum: 52-92-0F-5F-BB-CC-18-D6-B0-31-32-B7-87-C9-F2-63 */ ;

-  >>> turned assertion into assume statement

+  >>> MarkAsFullyVerified

 Processing command (at Snapshots5.v1.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3 /* checksum: 01-09-3B-C5-5F-C0-D6-24-82-98-EC-A1-9D-9B-D2-38 */ ;

-  >>> turned assertion into assume statement

+  >>> MarkAsFullyVerified

 Processing command (at Snapshots5.v1.dfy(20,40)) assert (exists b#5: bool :: b#5 || !b#5) || 4 != 4 /* checksum: 8A-FD-56-16-5D-AD-1D-FA-48-E5-4E-3E-7D-07-27-25 */ ;

-  >>> did nothing

+  >>> DoNothingToAssert

 Processing command (at Snapshots5.v1.dfy(22,38)) assert (exists b#7: bool :: b#7 || !b#7) || 5 != 5 /* checksum: 0F-FC-66-96-4A-EB-8E-10-F3-B4-D2-BC-A8-99-A8-FB */ ;

-  >>> did nothing

+  >>> DoNothingToAssert

 

 Dafny program verifier finished with 3 verified, 0 errors

 

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

 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

+  >>> DoNothingToAssert

 

 Dafny program verifier finished with 4 verified, 0 errors

 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

+  >>> DoNothingToAssert

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

 Execution trace:

     (0,0): anon0

@@ -167,11 +167,11 @@ Dafny program verifier finished with 3 verified, 1 error
 

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

 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

+  >>> DoNothingToAssert

 

 Dafny program verifier finished with 4 verified, 0 errors

 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

+  >>> DoNothingToAssert

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

 Execution trace:

     (0,0): anon0