1 files changed, 10 insertions, 8 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 7910f9c9..b83a7d52 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -141,6 +141,7 @@ namespace Microsoft.Boogie
       }

 

       tw.Write(errorInfo.Out.ToString());

+      tw.Write(errorInfo.Model.ToString());

       tw.Flush();

     }

 

@@ -235,6 +236,7 @@ namespace Microsoft.Boogie
     public ErrorKind Kind { get; set; }

     public string ImplementationName { get; set; }

     public TextWriter Out = new StringWriter();

+    public TextWriter Model = new StringWriter();

 

     public string FullMsg

     {

@@ -1016,7 +1018,7 @@ namespace Microsoft.Boogie
 

       #region Process the verification results and statistics

 

-      ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, output, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId);

+      ProcessOutcome(verificationResult.Outcome, verificationResult.Errors, TimeIndication(verificationResult), stats, output, impl.TimeLimit, er, verificationResult.ImplementationName, verificationResult.ImplementationToken, verificationResult.RequestId);

 

       ProcessErrors(verificationResult.Errors, verificationResult.Outcome, output, er, impl);

 

@@ -1139,7 +1141,7 @@ namespace Microsoft.Boogie
 

       foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)

       {

-        ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, er);

+        ProcessOutcome(x.outcome, x.errors, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er);

         ProcessErrors(x.errors, x.outcome, Console.Out, er);

       }

       //errorCount = outcome.ErrorCount;

@@ -1166,7 +1168,7 @@ namespace Microsoft.Boogie
       // Run Abstract Houdini

       var abs = new Houdini.AbsHoudini(program, domain);

       var absout = abs.ComputeSummaries();

-      ProcessOutcome(absout.outcome, absout.errors, "", stats, Console.Out, er);

+      ProcessOutcome(absout.outcome, absout.errors, "", stats, Console.Out, CommandLineOptions.Clo.ProverKillTime, er);

       ProcessErrors(absout.errors, absout.outcome, Console.Out, er);

 

       //Houdini.PredicateAbs.Initialize(program);

@@ -1195,7 +1197,7 @@ namespace Microsoft.Boogie
 

 

     private static void ProcessOutcome(VC.VCGen.Outcome outcome, List<Counterexample> errors, string timeIndication,

-                                       PipelineStatistics stats, TextWriter tw, ErrorReporterDelegate er = null, string implName = null, IToken implTok = null, string requestId = null)

+                                       PipelineStatistics stats, TextWriter tw, int timeLimit, ErrorReporterDelegate er = null, string implName = null, IToken implTok = null, string requestId = null)

     {

       Contract.Requires(stats != null);

 

@@ -1203,11 +1205,11 @@ namespace Microsoft.Boogie
 

       printer.Inform(timeIndication + OutcomeIndication(outcome, errors), tw);

 

-      ReportOutcome(outcome, er, implName, implTok, requestId, tw);

+      ReportOutcome(outcome, er, implName, implTok, requestId, tw, timeLimit);

     }

 

 

-    private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw)

+    private static void ReportOutcome(VC.VCGen.Outcome outcome, ErrorReporterDelegate er, string implName, IToken implTok, string requestId, TextWriter tw, int timeLimit)

     {

       ErrorInformation errorInfo = null;

 

@@ -1219,7 +1221,7 @@ namespace Microsoft.Boogie
         case VCGen.Outcome.TimedOut:

           if (implName != null && implTok != null)

           {

-            errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", CommandLineOptions.Clo.ProverKillTime, implName), requestId);

+            errorInfo = errorInformationFactory.CreateErrorInformation(implTok, string.Format("Verification timed out after {0} seconds ({1})", timeLimit, implName), requestId);

           }

           break;

         case VCGen.Outcome.OutOfMemory:

@@ -1352,7 +1354,7 @@ namespace Microsoft.Boogie
           }

           if (CommandLineOptions.Clo.ModelViewFile != null)

           {

-            error.PrintModel(errorInfo.Out);

+            error.PrintModel(errorInfo.Model);

           }

 

           printer.WriteErrorInformation(errorInfo, tw);