From 1f63aa9d54161eaeba72c339c649a7db96bca006 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Wed, 14 Oct 2009 22:42:49 +0000
Subject: 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.

---
 Source/Provers/Simplify/ProverInterface.ssc | 16 +++++++++-------
 Source/Provers/Z3/Prover.ssc                |  7 +------
 2 files changed, 10 insertions(+), 13 deletions(-)

(limited to 'Source')

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;
-- 
cgit v1.2.3