Make reveal axioms from opaque functions quantify over layers

1 files changed, 0 insertions, 25 deletions

diff --git a/Test/dafny0/FunctionSpecifications.dfy b/Test/dafny0/FunctionSpecifications.dfy
index caf8a681..1b7c8bfc 100644
--- a/Test/dafny0/FunctionSpecifications.dfy
+++ b/Test/dafny0/FunctionSpecifications.dfy
@@ -146,13 +146,6 @@ function {:opaque} f(i:int):int
   f(i) + 1

 }

 

-method m()

-  ensures false;

-{

-  reveal_f();

-  assert f(0) == f(0) + 1;

-}

-

 // Try a sneakier (nested) version of the test above

 function {:opaque} g(i:int):int

   decreases i;

@@ -165,13 +158,6 @@ function h(i:int):int
   g(i)

 }

 

-method n()

-  ensures false;

-{

-  reveal_g();

-  assert g(0) == g(0) + 1;

-}

-

 // Check that using the reveal_ lemma to prove the well-definedness of a function

 // in a lower SCC does not cause a soundness problem

 

@@ -188,14 +174,3 @@ function {:opaque} B(): int
   A()

 }

 

-method m_noreveal()

-  ensures false;

-{

-  assert f(0) == f(0) + 1;

-}

-

-method n_noreveal()

-  ensures false;

-{

-  assert g(0) == g(0) + 1;

-}