Changed how Boogie looks for Z3: first look in the directory where Boogie is being executed from, then look in "c:\Program Files\Microsoft Research\Z3-2.x\bin" for x := 5,4,3,2,1,0.

This fixes Issue Tracker item 5446.

2 files changed, 10 insertions, 13 deletions

diff --git a/Source/Provers/Simplify/ProverInterface.ssc b/Source/Provers/Simplify/ProverInterface.ssc
index 09873d7e..a3f38b9e 100644
--- a/Source/Provers/Simplify/ProverInterface.ssc
+++ b/Source/Provers/Simplify/ProverInterface.ssc
@@ -197,13 +197,15 @@ namespace Microsoft.Boogie.Simplify
       if (_proverPath == null) {

         // Initialize '_proverPath'

         _proverPath = Path.Combine(CodebaseString(), proverExe);

-        if (!File.Exists(_proverPath))

-        {

-          _proverPath = Path.Combine(@"c:\Program Files\Microsoft Research\Z3-2.0\bin", proverExe);

-        }

-        if (!File.Exists(_proverPath))

-        {

-          throw new ProverException("Cannot find executable: " + _proverPath);

+        string firstTry = _proverPath;

+        for (int minorVersion = 5; true; minorVersion--) {

+          if (File.Exists(_proverPath)) {

+            return;  // all seems good

+          }

+          if (minorVersion < 0) {

+            throw new ProverException("Cannot find executable: " + firstTry);

+          }

+          _proverPath = Path.Combine(@"c:\Program Files\Microsoft Research\Z3-2." + minorVersion + "\\bin", proverExe);

         }

       }

     }

diff --git a/Source/Provers/Z3/Prover.ssc b/Source/Provers/Z3/Prover.ssc
index c96369f8..a737b0ae 100644
--- a/Source/Provers/Z3/Prover.ssc
+++ b/Source/Provers/Z3/Prover.ssc
@@ -136,12 +136,7 @@ namespace Microsoft.Boogie.Z3
       cmdLineArgs = z3args;

       parameterSettings = parms;

       

-      string exePath = opts.ExeName;

-      if (!File.Exists(exePath)){

-        exePath = @"c:\Program Files\Microsoft Research\Z3-2.0\bin";

-      }

-      

-      ProcessStartInfo! psi = new ProcessStartInfo(exePath, z3args);

+      ProcessStartInfo! psi = new ProcessStartInfo(opts.ExeName, z3args);

       psi.CreateNoWindow = true;

       psi.UseShellExecute = false;

       psi.RedirectStandardInput = true;