Dafny:

* Modifies clause checking is now done with each update, instead of at the end of the method.  Not only does this improve error messages, but on some examples, it gives a dramatic speed-up (2x) in proving time.
* bugfix: range expressions of foreach statements were previously ignored during Translation

1 files changed, 5 insertions, 0 deletions

diff --git a/Source/DafnyDriver/DafnyDriver.ssc b/Source/DafnyDriver/DafnyDriver.ssc
index fa86c6e7..dc6e20b4 100644
--- a/Source/DafnyDriver/DafnyDriver.ssc
+++ b/Source/DafnyDriver/DafnyDriver.ssc
@@ -490,6 +490,11 @@ namespace Microsoft.Boogie
         program.Emit(new TokenTextWriter(Console.Out));

       }

 

+      if (CommandLineOptions.Clo.ExpandLambdas) {

+        LambdaHelper.ExpandLambdas(program);

+        //PrintBplFile ("-", program, true);

+      }

+

       // ---------- Verify ------------------------------------------------------------

 

       if (!CommandLineOptions.Clo.Verify) { return PipelineOutcome.Done; }