diff options
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 9 |
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));
+ }
}
}
|