Clean up a few thing and set proper defaults before merging

2 files changed, 6 insertions, 6 deletions

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index b2593705..a809cbd6 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -56,7 +56,7 @@ namespace Microsoft.Dafny
     public bool AllowGlobals = false;

     public bool CountVerificationErrors = true;

     public bool Optimize = false;

-    public bool AutoTriggers = true;

+    public bool AutoTriggers = false;

     public bool PrintTooltips = false;

 

     protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {

@@ -188,7 +188,7 @@ namespace Microsoft.Dafny
           return true;

 

         case "autoTriggers": {

-            int autoTriggers = 1; // defaults to reporting verification errors

+            int autoTriggers = 0;

             if (ps.GetNumericArgument(ref autoTriggers, 2)) {

               AutoTriggers = autoTriggers == 1;

             }

@@ -291,8 +291,8 @@ namespace Microsoft.Dafny
                 1 (default) - If preprocessing succeeds, set exit code to the number of

                               verification errors.

   /autoTriggers:<n>

-                0 - Do not generate {:trigger} annotations for user-level quantifiers.

-                1 (default) - Add a {:trigger} to each user-level quantifier. Existing

+                0 (default) - Do not generate {:trigger} annotations for user-level quantifiers.

+                1 - Add a {:trigger} to each user-level quantifier. Existing

                               annotations are preserved.

   /optimize     Produce optimized C# code, meaning:

                   - selects optimized C# prelude by passing 

diff --git a/Source/Dafny/TriggerGenerator.cs b/Source/Dafny/TriggerGenerator.cs
index d8a29d75..a777b4ae 100644
--- a/Source/Dafny/TriggerGenerator.cs
+++ b/Source/Dafny/TriggerGenerator.cs
@@ -25,7 +25,7 @@ using System.Diagnostics;
  */

 

 namespace Microsoft.Dafny {

-  class TriggerCandidate { // TODO Hashing is broken (duplicates can pop up)

+  class TriggerCandidate {

     internal Expression Expr;

     internal ISet<IVariable> Variables;

     internal List<ExprExtensions.TriggerMatch> MatchesInQuantifierBody;

@@ -35,7 +35,7 @@ namespace Microsoft.Dafny {
     }

   }

 

-  class TriggerCandidateComparer : IEqualityComparer<TriggerCandidate> {

+  class TriggerCandidateComparer : IEqualityComparer<TriggerCandidate> { //FIXME: There is a bunch of these comparers.

     private static TriggerCandidateComparer singleton;

     internal static TriggerCandidateComparer Instance {

       get { return singleton == null ? (singleton = new TriggerCandidateComparer()) : singleton; }