diff options
| author |  rustanleino <unknown> | 2010-06-08 18:05:23 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-06-08 18:05:23 +0000 |
| commit | 24ceefe6fac22e6361b1dc73b4bc878b1ba9aad5 (patch) | |
| tree | 8d063d83ed4cdfcd444984752ecec10813cbaabf /Source/Provers/Simplify | |
| parent | 0cddfa101560a1c2ca49729288766687361f2785 (diff) | |
Boogie:
* Look for Z3 versions up to 2.15 (but did not implement a better algorithm for it).
* Added prover-path output as part of /trace flag (that probably isn't the best command-line option for it).
Dafny:
* Split off some tests from Test/dafny0 into Test/dafny1.
* Added Test/dafny1/UltraFilter.dfy.
Diffstat (limited to 'Source/Provers/Simplify')
| -rw-r--r-- | Source/Provers/Simplify/ProverInterface.ssc | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/Source/Provers/Simplify/ProverInterface.ssc b/Source/Provers/Simplify/ProverInterface.ssc index c885f84e..bd618c24 100644 --- a/Source/Provers/Simplify/ProverInterface.ssc +++ b/Source/Provers/Simplify/ProverInterface.ssc @@ -207,22 +207,34 @@ namespace Microsoft.Boogie.Simplify programFiles = Environment.GetEnvironmentVariable("ProgramW6432");
}
- for (int minorVersion = 7; true; minorVersion--) {
+ List<string!> attempts = new List<string!>();
+ for (int minorVersion = 15; true; minorVersion--) {
if (File.Exists(_proverPath)) {
- return; // all seems good
+ break; // all seems good
}
+ attempts.Add(_proverPath);
if (minorVersion < 0) {
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("Failed to find prover. Looked in these places:");
+ foreach (string a in attempts) {
+ Console.WriteLine(" {0}", a);
+ }
+ }
throw new ProverException("Cannot find executable: " + firstTry);
}
_proverPath = Path.Combine(programFiles + @"\Microsoft Research\Z3-2." + minorVersion + @"\bin", proverExe);
if (File.Exists(_proverPath)) {
- return; // all seems good
+ break; // all seems good
}
+ attempts.Add(_proverPath);
if (programFilesX86 != null) {
_proverPath = Path.Combine(programFilesX86 + @"\Microsoft Research\Z3-2." + minorVersion + @"\bin", proverExe);
}
}
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("Using prover: " + _proverPath);
+ }
}
}
|