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 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

(limited to 'Source/Provers/Simplify')

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