Add the ability to specify how much "fuel" a function should have,

i.e., how many times Z3 is permitted to unfold it's definition.  The
new {:fuel} annotation can be added to the function itself, it which
case it will apply to all uses of that function, or it can overridden
within the scope of a module, function, method, iterator, calc, forall,
while, assert, or assume.  The general format is:

{:fuel functionName,lowFuel,highFuel}

When applied as an annotation to the function itself, omit functionName.
If highFuel is omitted, it defaults to lowFuel + 1.

The default fuel setting for recursive functions is 1,2.  Setting the fuel higher,
say, to 3,4, will give more unfoldings, which may make some proofs go through
with less programmer assistance (e.g., with fewer assert statements), but it may
also increase verification time, so use it with care.  Setting the fuel to 0,0 is
similar to making the definition opaque, except when used with all literal arguments.

1 files changed, 2 insertions, 0 deletions

diff --git a/Test/dafny4/Circ.dfy b/Test/dafny4/Circ.dfy
index e7609195..d110c05c 100644
--- a/Test/dafny4/Circ.dfy
+++ b/Test/dafny4/Circ.dfy
@@ -16,6 +16,7 @@ function zip(a: Stream, b: Stream): Stream { Cons(a.head, zip(b, a.tail)) }
 colemma BlinkZipProperty()

   ensures zip(zeros(), ones()) == blink();

 {

+    BlinkZipProperty();

 }

 

 // ----- Thue-Morse sequence -----

@@ -75,6 +76,7 @@ colemma FProperty(s: Stream<Bit>)
     // def. zip

     Cons(s.head, Cons(not(s).head, zip(s.tail, not(s).tail)));

   }

+  FProperty(s.tail);

 }

 

 // The fix-point theorem now follows easily.