Add PROVER_PATH prover option (to base options, but currently only used by SMTLib)

Add support for Inspector with latest Z3/SMT2 frontend

1 files changed, 4 insertions, 1 deletions

diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs
index 5b7fc946..f6a976e5 100644
--- a/Source/Core/VCExp.cs
+++ b/Source/Core/VCExp.cs
@@ -31,6 +31,7 @@ namespace Microsoft.Boogie {
     public int MemoryLimit = 0;

     public CommandLineOptions.BvHandling BitVectors = CommandLineOptions.BvHandling.None;

     public int Verbosity = 0;

+    public string ProverPath;

 

     private string/*!*/ stringRepr = "";

     [ContractInvariantMethod]

@@ -53,7 +54,8 @@ namespace Microsoft.Boogie {
              ParseBool(opt, "FORCE_LOG_STATUS", ref ForceLogStatus) ||

              ParseInt(opt, "MEMORY_LIMIT", ref MemoryLimit) ||

              ParseInt(opt, "VERBOSITY", ref Verbosity) ||

-             ParseInt(opt, "TIME_LIMIT", ref TimeLimit);

+             ParseInt(opt, "TIME_LIMIT", ref TimeLimit) || 

+             ParseString(opt, "PROVER_PATH", ref ProverPath);

       // || base.Parse(opt)

     }

 

@@ -73,6 +75,7 @@ APPEND_LOG_FILE=<bool>    Append, rather than overwrite the log file.
 MEMORY_LIMIT=<int>        Memory limit of the prover in megabytes.

 VERBOSITY=<int>           The higher, the more verbose.

 TIME_LIMIT=<int>          Time limit per verification condition in miliseconds.

+PROVER_PATH=<string>      Path to the prover to use.

 

 The generic options may or may not be used by the prover plugin.

 ";