Minor changes

2 files changed, 4 insertions, 4 deletions

diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index 8187db01..89f9a2c3 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1247,9 +1247,10 @@ namespace Microsoft.Boogie
       {

         lock (outputs)

         {

-          for (; nextPrintableIndex < outputs.Count() && outputs[nextPrintableIndex] != null; nextPrintableIndex++)

+          for (; nextPrintableIndex < outputs.Length && outputs[nextPrintableIndex] != null; nextPrintableIndex++)

           {

             Console.Write(outputs[nextPrintableIndex].ToString());

+            outputs[nextPrintableIndex] = null;

             Console.Out.Flush();

           }

         }

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index d66f68d3..226efa21 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -196,10 +196,10 @@ namespace Microsoft.Boogie
         {

           var desugaring = node.Desugaring;

           Contract.Assert(desugaring != null);

-          var precond = node.CheckedPrecondition(oldProc, Program);

+          var precond = node.CheckedPrecondition(oldProc, Program, e => FunctionExtractor.Extract(e, Program, axioms));

           if (precond != null)

           {

-            var assume = new AssumeCmd(node.tok, FunctionExtractor.Extract(precond, Program, axioms), new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));

+            var assume = new AssumeCmd(node.tok, precond, new QKeyValue(Token.NoToken, "precondition_previous_snapshot", new List<object>(), null));

             beforePrecondtionCheck.Add(assume);

           }

 

@@ -241,7 +241,6 @@ namespace Microsoft.Boogie
           node.AssignedAssumptionVariable = lv;

           currentImplementation.InjectAssumptionVariable(lv, !canUseSpecs);

           var lhs = new SimpleAssignLhs(Token.NoToken, new IdentifierExpr(Token.NoToken, lv));

-          // TODO(wuestholz): Try to extract functions for each clause.

           var rhs = LiteralExpr.And(new IdentifierExpr(Token.NoToken, lv), assumedExpr);

           var assumed = new AssignCmd(node.tok, new List<AssignLhs> { lhs }, new List<Expr> { rhs });

           after.Add(assumed);