Fix issue 93. Add per-function fuel setting that can be adjusted locally based

on context.

1 files changed, 2 insertions, 2 deletions

diff --git a/Test/dafny0/Fuel.dfy b/Test/dafny0/Fuel.dfy
index abbc831e..6347e134 100644
--- a/Test/dafny0/Fuel.dfy
+++ b/Test/dafny0/Fuel.dfy
@@ -126,7 +126,7 @@ module TestModule4 {
         requires y > 5;

         requires z < 0;

     {

-        assert {:fuel pos,0,0} pos(z) == 0;               // error: Should fail due to "opaque" fuel setting

+        assert {:fuel pos,0,0} pos(z) == 0;               // error: fuel can't be decreased

         assert pos(-1) == 0;

         if (*) {

             assert pos(y) == 3 + pos(y - 3);  // error: Should fail without extra fuel setting

@@ -404,7 +404,7 @@ module TestModule9 {
         requires y > 5;

         requires z < 0;

     {

-        assert {:fuel abs,0,0} abs(z) == -1*z;  // error: Cannot see the body of abs

+        assert {:fuel abs,0,0} abs(z) == -1*z;  // error: fuel can't be decreased

         assert abs(y) == y;     // Normal success

         assert abs(-1) == 1;    // lit bypasses fuel, so this should succeed

     }