cleaned up houdini options

1 files changed, 0 insertions, 37 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 56116601..e1136150 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -299,7 +299,6 @@ namespace Microsoft.Boogie {
     public int VcsCores = 1;

     public bool VcsDumpSplits = false;

 

-    public bool houdiniEnabled = false;

     public bool DebugRefuted = false;

 

     public XmlSink XmlRefuted {

@@ -401,7 +400,6 @@ namespace Microsoft.Boogie {
       Contract.Invariant(cce.NonNullElements(methodsToTranslateMethodQualified, true));

       Contract.Invariant(cce.NonNullElements(methodsToTranslateSubstring, true));

       Contract.Invariant(Ai != null);

-      Contract.Invariant(houdiniFlags != null);

     }

 

     [Rep]

@@ -441,13 +439,6 @@ namespace Microsoft.Boogie {
     }

     public AiFlags/*!*/ Ai = new AiFlags();

 

-    public class HoudiniFlags {

-      public bool continueAtError = false;

-      public bool incremental = false;

-    }

-

-    public HoudiniFlags/*!*/ houdiniFlags = new HoudiniFlags();

-

     [Verify(false)]

     private CommandLineOptions() {

       // this is just to suppress verification.

@@ -979,8 +970,6 @@ namespace Microsoft.Boogie {
           case "-contractInfer":

           case "/contractInfer":

             ContractInfer = true;

-            TheProverFactory = ProverFactory.Load("ContractInference");

-            ProverName = "ContractInference".ToUpper();

             break;

 

           case "-subsumption":

@@ -1367,28 +1356,6 @@ namespace Microsoft.Boogie {
             }

             break;

 

-          case "-Houdini":

-          case "/Houdini":

-            this.houdiniEnabled = true;

-            if (ps.hasColonArgument) {

-              if (ps.ConfirmArgumentCount(1)) {

-                foreach (char c in cce.NonNull(args[ps.i])) {

-                  switch (c) {

-                    case 'c':

-                      houdiniFlags.continueAtError = true;

-                      break;

-                    case 'i':

-                      houdiniFlags.incremental = true;

-                      break;

-                    default:

-                      ps.Error("Unknown houdini flag: " + c + "\n");

-                      break;

-                  }

-                }

-              }

-            }

-            break;

-

           case "-z3exe":

           case "/z3exe":

             if (ps.ConfirmArgumentCount(1)) {

@@ -2172,10 +2139,6 @@ namespace Microsoft.Boogie {
                          of every block

   /printInstrumented : print Boogie program after it has been

                    instrumented with invariants

-  /Houdini[:<flags>] : perform procedure Houdini

-                     c = continue when an error found

-                     i = use incremental queries

-  /dbgRefuted    : log refuted Houdini candidates to XmlSink

 

   ---- Debugging and general tracing options ---------------------------------