From 8ede9fda35767f083899940886b69f53640891c9 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Thu, 27 Aug 2015 18:59:10 -0700
Subject: Look for z3 in Binaries/z3/bin (but keep the vendored version for
 convenience)

Dafny now first looks for a z3 binary in z3/bin, and if it can't find one it
looks for one in Binaries/z3.exe (mostly for backwards-compatibility with
already set-up source installations).
---
 Source/DafnyDriver/DafnyDriver.cs | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'Source/DafnyDriver')

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 4b5ae8d8..c45d66fc 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -40,10 +40,11 @@ namespace Microsoft.Dafny
     public static int ThreadMain(string[] args)
     {
       Contract.Requires(cce.NonNullElements(args));
-         
+
+      ErrorReporter reporter = new ConsoleErrorReporter();
       ExecutionEngine.printer = new DafnyConsolePrinter(); // For boogie errors
 
-      DafnyOptions.Install(new DafnyOptions());
+      DafnyOptions.Install(new DafnyOptions(reporter));
 
       ExitValue exitValue = ExitValue.VERIFIED;
       CommandLineOptions.Clo.RunningBoogieFromCommandLine = true;
@@ -92,7 +93,7 @@ namespace Microsoft.Dafny
           goto END;
         }
       }
-      exitValue = ProcessFiles(CommandLineOptions.Clo.Files);
+      exitValue = ProcessFiles(CommandLineOptions.Clo.Files, reporter);
 
       END:
         if (CommandLineOptions.Clo.XmlSink != null) {
@@ -112,7 +113,7 @@ namespace Microsoft.Dafny
     }
 
 
-    static ExitValue ProcessFiles(IList<string/*!*/>/*!*/ fileNames, bool lookForSnapshots = true, string programId = null)
+    static ExitValue ProcessFiles(IList<string/*!*/>/*!*/ fileNames, ErrorReporter reporter, bool lookForSnapshots = true, string programId = null)
     {
       Contract.Requires(cce.NonNullElements(fileNames));
 
@@ -128,7 +129,7 @@ namespace Microsoft.Dafny
         {
           Console.WriteLine();
           Console.WriteLine("-------------------- {0} --------------------", f);
-          var ev = ProcessFiles(new List<string> { f }, lookForSnapshots, f);
+          var ev = ProcessFiles(new List<string> { f }, reporter, lookForSnapshots, f);
           if (exitValue != ev && ev != ExitValue.VERIFIED)
           {
             exitValue = ev;
@@ -142,7 +143,7 @@ namespace Microsoft.Dafny
         var snapshotsByVersion = ExecutionEngine.LookForSnapshots(fileNames);
         foreach (var s in snapshotsByVersion)
         {
-          var ev = ProcessFiles(new List<string>(s), false, programId);
+          var ev = ProcessFiles(new List<string>(s), reporter, false, programId);
           if (exitValue != ev && ev != ExitValue.VERIFIED)
           {
             exitValue = ev;
@@ -153,7 +154,6 @@ namespace Microsoft.Dafny
       
       using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count-1])) {
         Dafny.Program dafnyProgram;
-        ErrorReporter reporter = new ConsoleErrorReporter();
         string programName = fileNames.Count == 1 ? fileNames[0] : "the program";
         string err = Dafny.Main.ParseCheck(fileNames, programName, reporter, out dafnyProgram);
         if (err != null) {
-- 
cgit v1.2.3