DafnyExtension: Added a menu item to toggle verification result caching.

1 files changed, 6 insertions, 2 deletions

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index ad5986a8..f1db3316 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -38,8 +38,6 @@ namespace DafnyLanguage
         options.ApplyDefaultOptions();

 

         ExecutionEngine.printer = new ConsolePrinter();

-        // TODO(wuestholz): Turn this on as soon as the snapshot verification in Boogie works reliably.

-        // Dafny.DafnyOptions.Clo.VerifySnapshots = true;

       }

     }

 

@@ -155,6 +153,12 @@ namespace DafnyLanguage
       }

     }

 

+    public static bool ToggleIncrementalVerification()

+    {

+      Dafny.DafnyOptions.Clo.VerifySnapshots = !Dafny.DafnyOptions.Clo.VerifySnapshots;

+      return Dafny.DafnyOptions.Clo.VerifySnapshots;

+    }

+

     public static bool Verify(Dafny.Program dafnyProgram, string requestId, ErrorReporterDelegate er) {

       Dafny.Translator translator = new Dafny.Translator();

       translator.InsertChecksums = true;