adding z3name option

2 files changed, 11 insertions, 2 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index b57ea02a..309aab0e 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -484,6 +484,7 @@ namespace Microsoft.Boogie {
     public bool SimplifyLogFileAppend = false;

     public bool SoundnessSmokeTest = false;

     public string Z3ExecutablePath = null;

+    public string Z3ExecutableName = null;

     public string CVC4ExecutablePath = null;

     public int KInductionDepth = -1;

 

@@ -1551,8 +1552,15 @@ namespace Microsoft.Boogie {
             Z3ExecutablePath = args[ps.i];

           }

           return true;

+         // This sets name of z3 binary boogie binary directory, not path

+        case "z3name":

+          if (ps.ConfirmArgumentCount(1))

+          {

+              Z3ExecutableName = args[ps.i];

+          }

+          return true;

 

-		case "cvc4exe":

+        case "cvc4exe":

 			if (ps.ConfirmArgumentCount(1)) {

 				CVC4ExecutablePath = args[ps.i];

 			}

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index ffa4e0cb..bbc23917 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -52,7 +52,8 @@ namespace Microsoft.Boogie.SMTLib
                 return;

             }

 

-            var proverExe = "z3.exe";

+            var proverExe = CommandLineOptions.Clo.Z3ExecutableName; 

+            proverExe = proverExe == null ? "z3.exe" : proverExe;

 

             if (_proverPath == null)

             {