diff options
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 10 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 3 |
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)
{
|