Remove -z3DebugTraces and -z3Mam options (no longer working). Rename the -z3bv option to Z3-specific -proverOpt:OPTIMIZE_FOR_BV=true. Start with the prover-specific help (still needs changes in the yet-unconverted part).

1 files changed, 0 insertions, 31 deletions

diff --git a/Source/Core/CommandLineOptions.ssc b/Source/Core/CommandLineOptions.ssc
index c0ba6eaa..92d97fb1 100644
--- a/Source/Core/CommandLineOptions.ssc
+++ b/Source/Core/CommandLineOptions.ssc
@@ -95,8 +95,6 @@ namespace Microsoft.Boogie
     public bool SimplifyLogFileAppend = false;

     public bool SoundnessSmokeTest = false;

     

-    public List<string!>! Z3DebugTraces = new List<string!>();

-

     private bool noConsistencyChecks = false;

     public bool NoConsistencyChecks {

       get {return !Verify ? true : noConsistencyChecks;}

@@ -203,10 +201,8 @@ namespace Microsoft.Boogie
       get { if (DebugRefuted) return XmlSink; else return null; }

     }

     

-    public int Z3mam = 0;

     [Peer] public List<string!>! Z3Options = new List<string!>();

     public bool Z3types = false;

-    public bool Z3OptimizeForBitvectors = false;

     public int Z3lets = 3;  // 0 - none, 1 - only LET TERM, 2 - only LET FORMULA, 3 - (default) any

     invariant 0 <= Z3lets && Z3lets < 4;

 

@@ -926,13 +922,6 @@ namespace Microsoft.Boogie
             }

             break;

 

-          case "-z3DebugTrace":

-          case "/z3DebugTrace":

-          if (ps.ConfirmArgumentCount(1)) {

-              CommandLineOptions.Clo.Z3DebugTraces.Add((!)args[ps.i]);

-            }

-            break;

-            

           case "-inline":

           case "/inline":

             if (ps.ConfirmArgumentCount(1)) {

@@ -1125,19 +1114,6 @@ namespace Microsoft.Boogie
             ps.GetNumericArgument(ref ProverCCLimit);

             break;

             

-          case "-z3mam":

-          case "/z3mam":

-          {

-            int mam = 0;

-            if (ps.GetNumericArgument(ref mam)) {

-              if (mam == 0 || mam == 3 || mam == 4) {

-                Z3mam = mam;

-              } else

-                ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

-              }

-            }

-            break;

-          

           case "-z3opt":

           case "/z3opt":

             if (ps.ConfirmArgumentCount(1))

@@ -1237,7 +1213,6 @@ namespace Microsoft.Boogie
               ps.CheckBooleanFlag("causalImplies", ref CausalImplies) ||

               ps.CheckBooleanFlag("reflectAdd", ref ReflectAdd) ||

               ps.CheckBooleanFlag("z3types", ref Z3types) ||

-              ps.CheckBooleanFlag("z3bv", ref Z3OptimizeForBitvectors) ||

               ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||

               ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||

               ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) ||

@@ -2086,12 +2061,7 @@ namespace Microsoft.Boogie
   /simplifyMatchDepth:<num> : Set Simplify prover's matching depth limit

 

   Z3 specific options:

-  /z3mam:<num>   : Z3 matching engine: 0 (default) - eager instantiation,

-                   3 - lazy instantiation,

-                   4 - eager instantiation w/ matching-loop breaking heuristic

   /z3opt:<arg>   : specify additional Z3 options

-  /z3DebugTrace:<arg>   : z3 command line options so that Z3 generates debug

-                   tracing

   /z3multipleErrors : report multiple counterexamples for each error

   /useArrayTheory : use Z3's native theory (as opposed to axioms).  Currently

                     implies /monomorphize.

@@ -2104,7 +2074,6 @@ namespace Microsoft.Boogie
   /z3types       : generate multi-sorted VC that make use of Z3 types

   /z3lets:<n>    : 0 - no LETs, 1 - only LET TERM, 2 - only LET FORMULA,

                    3 - (default) any

-  /z3bv          : use Z3 settings optimized for bitvector reasoning

 ");

     }

   }