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.

1 files changed, 9 insertions, 7 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);

         }

       }

     }