Boogie: Present a nice error message when Z3 of lesser version than 3.2 is found

1 files changed, 9 insertions, 0 deletions

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index f9e90427..bbe13453 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -65,6 +65,8 @@ namespace Microsoft.Boogie.SMTLib
           z3Dirs.AddRange(Directory.GetDirectories(msrDir, "Z3-*"));

         }

 

+        int minMajor = 3, minMinor = 2;

+

         // Look for the most recent version of Z3.

         int minor = 0, major = 0;

         string winner = null;

@@ -86,6 +88,7 @@ namespace Microsoft.Boogie.SMTLib
         if (major == 0 && minor == 0) {

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

         }

+

         Contract.Assert(winner != null);

 

         _proverPath = Path.Combine(Path.Combine(winner, "bin"), proverExe);

@@ -96,6 +99,12 @@ namespace Microsoft.Boogie.SMTLib
         if (CommandLineOptions.Clo.Trace) {

           Console.WriteLine("[TRACE] Using prover: " + _proverPath);

         }

+

+        if (major < minMajor || (major == minMajor && minor < minMinor)) {

+          throw new ProverException(string.Format("Found version {0}.{1} of Z3. Please install version {0}.{1} or later. " +

+                                                  "(More conservative users might opt to supply -prover:Z3 option instead to get the historic Simplify back-end)", 

+                                                  major, minor, minMajor, minMinor));

+        }

       }

     }