diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-11-20 18:32:11 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-11-20 18:32:11 -0800 |
| commit | 04990f42dc81b2b46ceb81210278371c3d744a4f (patch) | |
| tree | b665593de7574119246aab7c3e72b3666061c02f /Source/Provers | |
| parent | 9527f8aea5086ab7addf0c058bf4b4df45960a49 (diff) | |
Incorporated contribution 3667, which fixes bug in /z3exe flag (http://boogie.codeplex.com/SourceControl/network/forks/stefanheule/boogiez3exefix/contribution/3667)
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 5dfec676..addfa3de 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -36,6 +36,18 @@ namespace Microsoft.Boogie.SMTLib {
Contract.Ensures(_proverPath != null);
+ // Command line option 'z3exe' always has priority if set
+ if (CommandLineOptions.Clo.Z3ExecutablePath != null) {
+ _proverPath = CommandLineOptions.Clo.Z3ExecutablePath;
+ if (!File.Exists(_proverPath)) {
+ throw new ProverException("Cannot find prover specified with z3exe: " + _proverPath);
+ }
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("[TRACE] Using prover: " + _proverPath);
+ }
+ return;
+ }
+
var proverExe = "z3.exe";
if (_proverPath == null) {
|