Split snapshot tests into separate files and add support for %S in runTests.py

37 files changed, 213 insertions, 218 deletions

diff --git a/Test/dafny0/snapshots/Snapshots0.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots0.v0.dfy
index 73db9f9c..73db9f9c 100644
--- a/Test/dafny0/snapshots/Snapshots0.v0.dfy
+++ b/Test/dafny0/snapshots/Inputs/Snapshots0.v0.dfy
diff --git a/Test/dafny0/snapshots/Snapshots0.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots0.v1.dfy
index db9fc01a..db9fc01a 100644
--- a/Test/dafny0/snapshots/Snapshots0.v1.dfy
+++ b/Test/dafny0/snapshots/Inputs/Snapshots0.v1.dfy
diff --git a/Test/dafny0/snapshots/Snapshots1.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots1.v0.dfy
index 34d066c3..34d066c3 100644
--- a/Test/dafny0/snapshots/Snapshots1.v0.dfy
+++ b/Test/dafny0/snapshots/Inputs/Snapshots1.v0.dfy
diff --git a/Test/dafny0/snapshots/Snapshots1.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots1.v1.dfy
index 184ac65d..184ac65d 100644
--- a/Test/dafny0/snapshots/Snapshots1.v1.dfy
+++ b/Test/dafny0/snapshots/Inputs/Snapshots1.v1.dfy
diff --git a/Test/dafny0/snapshots/Snapshots2.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots2.v0.dfy
index 727e177d..727e177d 100644
--- a/Test/dafny0/snapshots/Snapshots2.v0.dfy
+++ b/Test/dafny0/snapshots/Inputs/Snapshots2.v0.dfy
diff --git a/Test/dafny0/snapshots/Snapshots2.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots2.v1.dfy
index 02a91b52..02a91b52 100644
--- a/Test/dafny0/snapshots/Snapshots2.v1.dfy
+++ b/Test/dafny0/snapshots/Inputs/Snapshots2.v1.dfy
diff --git a/Test/dafny0/snapshots/Snapshots3.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots3.v0.dfy
index 72607412..72607412 100644
--- a/Test/dafny0/snapshots/Snapshots3.v0.dfy
+++ b/Test/dafny0/snapshots/Inputs/Snapshots3.v0.dfy
diff --git a/Test/dafny0/snapshots/Snapshots3.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots3.v1.dfy
index 3b186318..3b186318 100644
--- a/Test/dafny0/snapshots/Snapshots3.v1.dfy
+++ b/Test/dafny0/snapshots/Inputs/Snapshots3.v1.dfy
diff --git a/Test/dafny0/snapshots/Snapshots4.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots4.v0.dfy
index beaadfeb..beaadfeb 100644
--- a/Test/dafny0/snapshots/Snapshots4.v0.dfy
+++ b/Test/dafny0/snapshots/Inputs/Snapshots4.v0.dfy
diff --git a/Test/dafny0/snapshots/Snapshots4.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots4.v1.dfy
index cf9ae753..cf9ae753 100644
--- a/Test/dafny0/snapshots/Snapshots4.v1.dfy
+++ b/Test/dafny0/snapshots/Inputs/Snapshots4.v1.dfy
diff --git a/Test/dafny0/snapshots/Snapshots5.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots5.v0.dfy
index b81c1a2b..b81c1a2b 100644
--- a/Test/dafny0/snapshots/Snapshots5.v0.dfy
+++ b/Test/dafny0/snapshots/Inputs/Snapshots5.v0.dfy
diff --git a/Test/dafny0/snapshots/Snapshots5.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy
index 05dbced0..05dbced0 100644
--- a/Test/dafny0/snapshots/Snapshots5.v1.dfy
+++ b/Test/dafny0/snapshots/Inputs/Snapshots5.v1.dfy
diff --git a/Test/dafny0/snapshots/Snapshots6.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots6.v0.dfy
index c3742f4b..c3742f4b 100644
--- a/Test/dafny0/snapshots/Snapshots6.v0.dfy
+++ b/Test/dafny0/snapshots/Inputs/Snapshots6.v0.dfy
diff --git a/Test/dafny0/snapshots/Snapshots6.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots6.v1.dfy
index aeb520cb..aeb520cb 100644
--- a/Test/dafny0/snapshots/Snapshots6.v1.dfy
+++ b/Test/dafny0/snapshots/Inputs/Snapshots6.v1.dfy
diff --git a/Test/dafny0/snapshots/Snapshots7.v0.dfy b/Test/dafny0/snapshots/Inputs/Snapshots7.v0.dfy
index 27c7da5f..27c7da5f 100644
--- a/Test/dafny0/snapshots/Snapshots7.v0.dfy
+++ b/Test/dafny0/snapshots/Inputs/Snapshots7.v0.dfy
diff --git a/Test/dafny0/snapshots/Snapshots7.v1.dfy b/Test/dafny0/snapshots/Inputs/Snapshots7.v1.dfy
index b45dfe78..b45dfe78 100644
--- a/Test/dafny0/snapshots/Snapshots7.v1.dfy
+++ b/Test/dafny0/snapshots/Inputs/Snapshots7.v1.dfy
diff --git a/Test/dafny0/snapshots/Snapshots0.run.dfy b/Test/dafny0/snapshots/Snapshots0.run.dfy
new file mode 100644
index 00000000..cb96468e
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots0.run.dfy
@@ -0,0 +1,2 @@
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots0.dfy > "%t"

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

diff --git a/Test/dafny0/snapshots/Snapshots0.run.dfy.expect b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect
new file mode 100644
index 00000000..96c280d9
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots0.run.dfy.expect
@@ -0,0 +1,25 @@
+Processing command (at Snapshots0.v0.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+  >>> DoNothingToAssert

+Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false);

+  >>> DoNothingToAssert

+

+Dafny program verifier finished with 3 verified, 0 errors

+Processing implementation CheckWellformed$$_module.__default.bar (at Snapshots0.v1.dfy(7,8)):

+  >>> added axiom: ##extracted_function##1() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight)

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1();

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

+  >>> added axiom: (forall call0old#AT#$Heap: Heap, $Heap: Heap :: {:weight 30} { ##extracted_function##2(call0old#AT#$Heap, $Heap) } ##extracted_function##2(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call0old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call0old#AT#$Heap, $o, $f)) && $HeapSucc(call0old#AT#$Heap, $Heap)))

+  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0old#AT#$Heap, $Heap);

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1();

+  >>> AssumeNegationOfAssumptionVariable

+Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+  >>> MarkAsFullyVerified

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call0old#AT#$Heap, $Heap);

+  >>> AssumeNegationOfAssumptionVariable

+Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false);

+  >>> MarkAsPartiallyVerified

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

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 2 verified, 1 error

diff --git a/Test/dafny0/snapshots/Snapshots1.run.dfy b/Test/dafny0/snapshots/Snapshots1.run.dfy
new file mode 100644
index 00000000..7c277b3e
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots1.run.dfy
@@ -0,0 +1,2 @@
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots1.dfy > "%t"

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

diff --git a/Test/dafny0/snapshots/Snapshots1.run.dfy.expect b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect
new file mode 100644
index 00000000..878f9905
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots1.run.dfy.expect
@@ -0,0 +1,21 @@
+Processing command (at Snapshots1.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+  >>> DoNothingToAssert

+Processing command (at Snapshots1.v0.dfy(4,10)) assert Lit(false);

+  >>> DoNothingToAssert

+Processing command (at Snapshots1.v0.dfy(12,3)) assert true;

+  >>> 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,4)):

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

+Processing command (at Snapshots1.v1.dfy(12,3)) assert true;

+  >>> MarkAsFullyVerified

+Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+  >>> MarkAsFullyVerified

+Processing command (at Snapshots1.v1.dfy(4,10)) assert Lit(false);

+  >>> DoNothingToAssert

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

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 3 verified, 1 error

diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy b/Test/dafny0/snapshots/Snapshots2.run.dfy
new file mode 100644
index 00000000..889a8153
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots2.run.dfy
@@ -0,0 +1,2 @@
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots2.dfy > "%t"

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

diff --git a/Test/dafny0/snapshots/Snapshots2.run.dfy.expect b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect
new file mode 100644
index 00000000..a6a9bc4c
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots2.run.dfy.expect
@@ -0,0 +1,41 @@
+Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+  >>> DoNothingToAssert

+Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false);

+  >>> DoNothingToAssert

+Processing command (at Snapshots2.v0.dfy(11,11)) assert true;

+  >>> DoNothingToAssert

+Processing command (at Snapshots2.v0.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap);

+  >>> DoNothingToAssert

+Processing command (at Snapshots2.v0.dfy(14,11)) assert true;

+  >>> DoNothingToAssert

+Processing command (at Snapshots2.v0.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap));

+  >>> DoNothingToAssert

+Processing command (at Snapshots2.v0.dfy(18,3)) assert true;

+  >>> 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,4)):

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

+Processing implementation CheckWellformed$$_module.__default.P (at Snapshots2.v1.dfy(10,11)):

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;

+Processing implementation CheckWellformed$$_module.__default.Q (at Snapshots2.v1.dfy(13,11)):

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;

+Processing command (at Snapshots2.v1.dfy(18,3)) assert true;

+  >>> MarkAsFullyVerified

+Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+  >>> MarkAsFullyVerified

+Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false);

+  >>> DoNothingToAssert

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

+Execution trace:

+    (0,0): anon0

+Processing command (at Snapshots2.v1.dfy(11,11)) assert true;

+  >>> DoNothingToAssert

+Processing command (at Snapshots2.v1.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap);

+  >>> DoNothingToAssert

+Processing command (at Snapshots2.v1.dfy(14,11)) assert true;

+  >>> DoNothingToAssert

+Processing command (at Snapshots2.v1.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap));

+  >>> DoNothingToAssert

+

+Dafny program verifier finished with 5 verified, 1 error

diff --git a/Test/dafny0/snapshots/Snapshots3.run.dfy b/Test/dafny0/snapshots/Snapshots3.run.dfy
new file mode 100644
index 00000000..3df182d6
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots3.run.dfy
@@ -0,0 +1,2 @@
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots3.dfy > "%t"

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

diff --git a/Test/dafny0/snapshots/Snapshots3.run.dfy.expect b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect
new file mode 100644
index 00000000..07e2d063
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots3.run.dfy.expect
@@ -0,0 +1,18 @@
+Processing command (at Snapshots3.v0.dfy(9,14)) assert Lit(0 != 0);

+  >>> DoNothingToAssert

+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

+Processing command (at Snapshots3.v1.dfy(5,12)) assert Lit(true);

+  >>> DoNothingToAssert

+Processing command (at Snapshots3.v1.dfy(9,14)) assert Lit(0 != 0);

+  >>> RecycleError

+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

diff --git a/Test/dafny0/snapshots/Snapshots4.run.dfy b/Test/dafny0/snapshots/Snapshots4.run.dfy
new file mode 100644
index 00000000..fd6bef41
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots4.run.dfy
@@ -0,0 +1,2 @@
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots4.dfy > "%t"

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

diff --git a/Test/dafny0/snapshots/Snapshots4.run.dfy.expect b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect
new file mode 100644
index 00000000..fdc97775
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots4.run.dfy.expect
@@ -0,0 +1,20 @@
+Processing command (at Snapshots4.v0.dfy(9,14)) assert LitInt(0) == LitInt(0);

+  >>> DoNothingToAssert

+

+Dafny program verifier finished with 2 verified, 0 errors

+Processing command (at Snapshots4.v1.dfy(5,14)) assert Lit(1 != 1);

+  >>> DoNothingToAssert

+Processing command (at Snapshots4.v1.dfy(9,14)) assert LitInt(0) == LitInt(0);

+  >>> MarkAsFullyVerified

+Processing command (at Snapshots4.v1.dfy(10,14)) assert Lit(2 != 2);

+  >>> DoNothingToAssert

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+

+Dafny program verifier finished with 1 verified, 2 errors

diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy b/Test/dafny0/snapshots/Snapshots5.run.dfy
new file mode 100644
index 00000000..4f26aac4
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots5.run.dfy
@@ -0,0 +1,2 @@
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots5.dfy > "%t"

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

diff --git a/Test/dafny0/snapshots/Snapshots5.run.dfy.expect b/Test/dafny0/snapshots/Snapshots5.run.dfy.expect
new file mode 100644
index 00000000..2ad73416
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots5.run.dfy.expect
@@ -0,0 +1,26 @@
+Processing command (at Snapshots5.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+  >>> DoNothingToAssert

+Processing command (at Snapshots5.v0.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;

+  >>> DoNothingToAssert

+Processing command (at Snapshots5.v0.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+  >>> DoNothingToAssert

+Processing command (at Snapshots5.v0.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;

+  >>> DoNothingToAssert

+Processing command (at Snapshots5.v0.dfy(20,40)) assert (forall b#5: bool :: true ==> b#5 || !b#5) || 1 != 1;

+  >>> DoNothingToAssert

+

+Dafny program verifier finished with 3 verified, 0 errors

+Processing command (at Snapshots5.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+  >>> MarkAsFullyVerified

+Processing command (at Snapshots5.v1.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;

+  >>> MarkAsFullyVerified

+Processing command (at Snapshots5.v1.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

+  >>> MarkAsFullyVerified

+Processing command (at Snapshots5.v1.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;

+  >>> MarkAsFullyVerified

+Processing command (at Snapshots5.v1.dfy(20,40)) assert (exists b#5: bool :: b#5 || !b#5) || 4 != 4;

+  >>> DoNothingToAssert

+Processing command (at Snapshots5.v1.dfy(22,38)) assert (exists b#7: bool :: b#7 || !b#7) || 5 != 5;

+  >>> DoNothingToAssert

+

+Dafny program verifier finished with 3 verified, 0 errors

diff --git a/Test/dafny0/snapshots/Snapshots6.run.dfy b/Test/dafny0/snapshots/Snapshots6.run.dfy
new file mode 100644
index 00000000..157fc5b7
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots6.run.dfy
@@ -0,0 +1,2 @@
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots6.dfy > "%t"

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

diff --git a/Test/dafny0/snapshots/Snapshots6.run.dfy.expect b/Test/dafny0/snapshots/Snapshots6.run.dfy.expect
new file mode 100644
index 00000000..af440327
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots6.run.dfy.expect
@@ -0,0 +1,11 @@
+Processing command (at Snapshots6.v0.dfy(20,14)) assert Lit(false);

+  >>> DoNothingToAssert

+

+Dafny program verifier finished with 4 verified, 0 errors

+Processing command (at Snapshots6.v1.dfy(20,14)) assert Lit(false);

+  >>> DoNothingToAssert

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

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 3 verified, 1 error

diff --git a/Test/dafny0/snapshots/Snapshots7.run.dfy b/Test/dafny0/snapshots/Snapshots7.run.dfy
new file mode 100644
index 00000000..b192f090
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots7.run.dfy
@@ -0,0 +1,2 @@
+// RUN: %dafny /compile:0 /verifySnapshots:2 /traceCaching:1 %S/Inputs/Snapshots7.dfy > "%t"

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

diff --git a/Test/dafny0/snapshots/Snapshots7.run.dfy.expect b/Test/dafny0/snapshots/Snapshots7.run.dfy.expect
new file mode 100644
index 00000000..7c073a9a
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots7.run.dfy.expect
@@ -0,0 +1,31 @@
+Processing command (at Snapshots7.v0.dfy(19,14)) assert Lit(false);

+  >>> DoNothingToAssert

+

+Dafny program verifier finished with 4 verified, 0 errors

+Processing implementation CheckWellformed$$_0_M0.C.Foo (at Snapshots7.v1.dfy(5,12)):

+  >>> added axiom: ##extracted_function##1() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight)

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1();

+Processing implementation Impl$$_0_M0.C.Foo (at Snapshots7.v1.dfy(5,12)):

+  >>> added axiom: ##extracted_function##2() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight && Lit(false))

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##2();

+Processing implementation CheckWellformed$$_1_M1.C.Foo (at Snapshots7.v1.dfy[M1](5,12)):

+  >>> added axiom: ##extracted_function##3() == (1 == $ModuleContextHeight && 0 == $FunctionContextHeight)

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##3();

+Processing implementation Impl$$_1_M1.C.Foo (at Snapshots7.v1.dfy[M1](5,12)):

+  >>> added axiom: ##extracted_function##4() == (1 == $ModuleContextHeight && 0 == $FunctionContextHeight && Lit(false))

+  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##4();

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1();

+  >>> AssumeNegationOfAssumptionVariable

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2();

+  >>> AssumeNegationOfAssumptionVariable

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##3();

+  >>> AssumeNegationOfAssumptionVariable

+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##4();

+  >>> AssumeNegationOfAssumptionVariable

+Processing command (at Snapshots7.v1.dfy(19,14)) assert Lit(false);

+  >>> MarkAsPartiallyVerified

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

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 3 verified, 1 error

diff --git a/Test/dafny0/snapshots/lit.local.cfg b/Test/dafny0/snapshots/lit.local.cfg
deleted file mode 100644
index 07cb869f..00000000
--- a/Test/dafny0/snapshots/lit.local.cfg
+++ /dev/null
@@ -1,5 +0,0 @@
-# This test is unusual in that we don't use the .bpl files
-# directly on the command line. So instead we'll invoke
-# files in this directory with extension '.snapshot'. There
-# will only be one for now
-config.suffixes = ['.snapshot']
diff --git a/Test/dafny0/snapshots/runtest.snapshot b/Test/dafny0/snapshots/runtest.snapshot
deleted file mode 100644
index 62ccabb3..00000000
--- a/Test/dafny0/snapshots/runtest.snapshot
+++ /dev/null
@@ -1,2 +0,0 @@
-// 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
deleted file mode 100644
index f1050f62..00000000
--- a/Test/dafny0/snapshots/runtest.snapshot.expect
+++ /dev/null
@@ -1,209 +0,0 @@
-

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

-Processing command (at Snapshots0.v0.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

-  >>> DoNothingToAssert

-Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false);

-  >>> DoNothingToAssert

-

-Dafny program verifier finished with 3 verified, 0 errors

-Processing implementation CheckWellformed$$_module.__default.bar (at Snapshots0.v1.dfy(7,8)):

-  >>> added axiom: ##extracted_function##1() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight)

-  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1();

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

-  >>> added axiom: (forall call0old#AT#$Heap: Heap, $Heap: Heap :: {:weight 30} { ##extracted_function##2(call0old#AT#$Heap, $Heap) } ##extracted_function##2(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call0old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call0old#AT#$Heap, $o, $f)) && $HeapSucc(call0old#AT#$Heap, $Heap)))

-  >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0old#AT#$Heap, $Heap);

-Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1();

-  >>> AssumeNegationOfAssumptionVariable

-Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

-  >>> MarkAsFullyVerified

-Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call0old#AT#$Heap, $Heap);

-  >>> AssumeNegationOfAssumptionVariable

-Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false);

-  >>> MarkAsPartiallyVerified

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

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 2 verified, 1 error

-

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

-Processing command (at Snapshots1.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

-  >>> DoNothingToAssert

-Processing command (at Snapshots1.v0.dfy(4,10)) assert Lit(false);

-  >>> DoNothingToAssert

-Processing command (at Snapshots1.v0.dfy(12,3)) assert true;

-  >>> 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,4)):

-  >>> added after: a##cached##0 := a##cached##0 && false;

-Processing command (at Snapshots1.v1.dfy(12,3)) assert true;

-  >>> MarkAsFullyVerified

-Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

-  >>> MarkAsFullyVerified

-Processing command (at Snapshots1.v1.dfy(4,10)) assert Lit(false);

-  >>> DoNothingToAssert

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

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 3 verified, 1 error

-

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

-Processing command (at Snapshots2.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

-  >>> DoNothingToAssert

-Processing command (at Snapshots2.v0.dfy(4,10)) assert Lit(false);

-  >>> DoNothingToAssert

-Processing command (at Snapshots2.v0.dfy(11,11)) assert true;

-  >>> DoNothingToAssert

-Processing command (at Snapshots2.v0.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap);

-  >>> DoNothingToAssert

-Processing command (at Snapshots2.v0.dfy(14,11)) assert true;

-  >>> DoNothingToAssert

-Processing command (at Snapshots2.v0.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap));

-  >>> DoNothingToAssert

-Processing command (at Snapshots2.v0.dfy(18,3)) assert true;

-  >>> 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,4)):

-  >>> added after: a##cached##0 := a##cached##0 && false;

-Processing implementation CheckWellformed$$_module.__default.P (at Snapshots2.v1.dfy(10,11)):

-  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;

-Processing implementation CheckWellformed$$_module.__default.Q (at Snapshots2.v1.dfy(13,11)):

-  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;

-Processing command (at Snapshots2.v1.dfy(18,3)) assert true;

-  >>> MarkAsFullyVerified

-Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

-  >>> MarkAsFullyVerified

-Processing command (at Snapshots2.v1.dfy(4,10)) assert Lit(false);

-  >>> DoNothingToAssert

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

-Execution trace:

-    (0,0): anon0

-Processing command (at Snapshots2.v1.dfy(11,11)) assert true;

-  >>> DoNothingToAssert

-Processing command (at Snapshots2.v1.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap);

-  >>> DoNothingToAssert

-Processing command (at Snapshots2.v1.dfy(14,11)) assert true;

-  >>> DoNothingToAssert

-Processing command (at Snapshots2.v1.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap));

-  >>> DoNothingToAssert

-

-Dafny program verifier finished with 5 verified, 1 error

-

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

-Processing command (at Snapshots3.v0.dfy(9,14)) assert Lit(0 != 0);

-  >>> DoNothingToAssert

-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

-Processing command (at Snapshots3.v1.dfy(5,12)) assert Lit(true);

-  >>> DoNothingToAssert

-Processing command (at Snapshots3.v1.dfy(9,14)) assert Lit(0 != 0);

-  >>> RecycleError

-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

-

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

-Processing command (at Snapshots4.v0.dfy(9,14)) assert LitInt(0) == LitInt(0);

-  >>> DoNothingToAssert

-

-Dafny program verifier finished with 2 verified, 0 errors

-Processing command (at Snapshots4.v1.dfy(5,14)) assert Lit(1 != 1);

-  >>> DoNothingToAssert

-Processing command (at Snapshots4.v1.dfy(9,14)) assert LitInt(0) == LitInt(0);

-  >>> MarkAsFullyVerified

-Processing command (at Snapshots4.v1.dfy(10,14)) assert Lit(2 != 2);

-  >>> DoNothingToAssert

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

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Then

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

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3_Else

-

-Dafny program verifier finished with 1 verified, 2 errors

-

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

-Processing command (at Snapshots5.v0.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

-  >>> DoNothingToAssert

-Processing command (at Snapshots5.v0.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;

-  >>> DoNothingToAssert

-Processing command (at Snapshots5.v0.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

-  >>> DoNothingToAssert

-Processing command (at Snapshots5.v0.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;

-  >>> DoNothingToAssert

-Processing command (at Snapshots5.v0.dfy(20,40)) assert (forall b#5: bool :: true ==> b#5 || !b#5) || 1 != 1;

-  >>> DoNothingToAssert

-

-Dafny program verifier finished with 3 verified, 0 errors

-Processing command (at Snapshots5.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

-  >>> MarkAsFullyVerified

-Processing command (at Snapshots5.v1.dfy(10,40)) assert (forall b#1: bool :: true ==> b#1 || !b#1) || 0 != 0;

-  >>> MarkAsFullyVerified

-Processing command (at Snapshots5.v1.dfy(12,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);

-  >>> MarkAsFullyVerified

-Processing command (at Snapshots5.v1.dfy(13,38)) assert (forall b#3: bool :: true ==> b#3 || !b#3) || 3 != 3;

-  >>> MarkAsFullyVerified

-Processing command (at Snapshots5.v1.dfy(20,40)) assert (exists b#5: bool :: b#5 || !b#5) || 4 != 4;

-  >>> DoNothingToAssert

-Processing command (at Snapshots5.v1.dfy(22,38)) assert (exists b#7: bool :: b#7 || !b#7) || 5 != 5;

-  >>> DoNothingToAssert

-

-Dafny program verifier finished with 3 verified, 0 errors

-

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

-Processing command (at Snapshots6.v0.dfy(20,14)) assert Lit(false);

-  >>> DoNothingToAssert

-

-Dafny program verifier finished with 4 verified, 0 errors

-Processing command (at Snapshots6.v1.dfy(20,14)) assert Lit(false);

-  >>> DoNothingToAssert

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

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 3 verified, 1 error

-

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

-Processing command (at Snapshots7.v0.dfy(19,14)) assert Lit(false);

-  >>> DoNothingToAssert

-

-Dafny program verifier finished with 4 verified, 0 errors

-Processing implementation CheckWellformed$$_0_M0.C.Foo (at Snapshots7.v1.dfy(5,12)):

-  >>> added axiom: ##extracted_function##1() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight)

-  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1();

-Processing implementation Impl$$_0_M0.C.Foo (at Snapshots7.v1.dfy(5,12)):

-  >>> added axiom: ##extracted_function##2() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight && Lit(false))

-  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##2();

-Processing implementation CheckWellformed$$_1_M1.C.Foo (at Snapshots7.v1.dfy[M1](5,12)):

-  >>> added axiom: ##extracted_function##3() == (1 == $ModuleContextHeight && 0 == $FunctionContextHeight)

-  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##3();

-Processing implementation Impl$$_1_M1.C.Foo (at Snapshots7.v1.dfy[M1](5,12)):

-  >>> added axiom: ##extracted_function##4() == (1 == $ModuleContextHeight && 0 == $FunctionContextHeight && Lit(false))

-  >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##4();

-Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1();

-  >>> AssumeNegationOfAssumptionVariable

-Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2();

-  >>> AssumeNegationOfAssumptionVariable

-Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##3();

-  >>> AssumeNegationOfAssumptionVariable

-Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##4();

-  >>> AssumeNegationOfAssumptionVariable

-Processing command (at Snapshots7.v1.dfy(19,14)) assert Lit(false);

-  >>> MarkAsPartiallyVerified

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

-Execution trace:

-    (0,0): anon0

-

-Dafny program verifier finished with 3 verified, 1 error

diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg
index 1fe593f4..a960bdbc 100644
--- a/Test/lit.site.cfg
+++ b/Test/lit.site.cfg
@@ -22,7 +22,7 @@ config.suffixes = ['.dfy']
 # excludes: A list of directories to exclude from the testsuite. The 'Inputs'
 # subdirectories contain auxiliary inputs for various tests in their parent
 # directories.
-config.excludes = []
+config.excludes = ['Inputs']
 
 # test_source_root: The root path where tests are located.
 config.test_source_root = os.path.dirname(os.path.abspath(__file__))
diff --git a/Test/runTests.py b/Test/runTests.py
index b8d8e6f4..d2bb61c9 100644
--- a/Test/runTests.py
+++ b/Test/runTests.py
@@ -34,7 +34,7 @@ except ImportError:
         pass

 

 class Defaults:

-    ALWAYS_EXCLUDED = ["Output", "snapshots", "sandbox", "desktop"]

+    ALWAYS_EXCLUDED = ["Inputs", "Output", "sandbox", "desktop"]

     DAFNY_BIN = os.path.realpath(os.path.join(os.path.dirname(__file__), "../Binaries/Dafny.exe"))

     COMPILER = [DAFNY_BIN]

     FLAGS = ["/useBaseNameForFileName", "/compile:1", "/nologo", "/timeLimit:120"]

@@ -108,7 +108,9 @@ class Test:
         self.timeout = timeout

         self.compiler_id = compiler_id

         self.cmds = [cmd.replace("%s", self.source_path) for cmd in self.cmds]

+        self.cmds = [cmd.replace("%S", self.source_directory) for cmd in self.cmds]

         self.cmds = [cmd.replace("%t", self.temp_output_path) for cmd in self.cmds]

+        self.cmds = [cmd.replace("%T", self.temp_directory) for cmd in self.cmds]

 

         self.status = TestStatus.PENDING

         self.proc_info = platform.processor()