Added a test.

1 files changed, 27 insertions, 0 deletions

diff --git a/Test/dafny0/snapshots/Snapshots5.v1.dfy b/Test/dafny0/snapshots/Snapshots5.v1.dfy
new file mode 100644
index 00000000..05dbced0
--- /dev/null
+++ b/Test/dafny0/snapshots/Snapshots5.v1.dfy
@@ -0,0 +1,27 @@
+method M()

+{

+  N();

+  if (*)

+  {

+

+  }

+  else

+  {

+    assert (forall b: bool :: b || !b) || 0 != 0;

+  }

+  N();

+  assert (forall b: bool :: b || !b) || 3 != 3;

+  if (*)

+  {

+

+  }

+  else

+  {

+    assert (exists b: bool :: b || !b) || 4 != 4;

+  }

+  assert (exists b: bool :: b || !b) || 5 != 5;

+}

+

+

+method N()

+  ensures (forall b: bool :: b || !b) || 2 != 2;