Minor changes

3 files changed, 13 insertions, 10 deletions

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 746e70c0..900d1c7a 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -2640,18 +2640,21 @@ namespace Microsoft.Boogie {
       Substitution substOldCombined = v => { Expr s; if (oldSubst.TryGetValue(v, out s)) { return s; } return calleeSubstitutionOld(v); };

 

       var clauses = procedure.Ensures.Select(e => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, substOldCombined, e.Condition, program)).Concat(modifies);

-      var conj = Conjunction(clauses);

       // TODO(wuestholz): Try extracting a function for each clause:

-      // var conj = Conjunction(clauses.Select(c => extract(c)));

+      // return Conjunction(clauses.Select(c => extract(c)));

+      var conj = Conjunction(clauses);

       return conj != null ? extract(conj) : conj;

     }

 

-    public Expr CheckedPrecondition(Procedure procedure, Program program)

+    public Expr CheckedPrecondition(Procedure procedure, Program program, Func<Expr, Expr> extract)

     {

-      Contract.Requires(calleeSubstitution != null && calleeSubstitutionOld != null && program != null);

+      Contract.Requires(calleeSubstitution != null && calleeSubstitutionOld != null && program != null && extract != null);

 

-      var requires = procedure.Requires.Where(r => !r.Free).Select(r => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, r.Condition, program));

-      return Conjunction(requires);

+      var clauses = procedure.Requires.Where(r => !r.Free).Select(r => Substituter.FunctionCallReresolvingApplyReplacingOldExprs(calleeSubstitution, calleeSubstitutionOld, r.Condition, program));

+      // TODO(wuestholz): Try extracting a function for each clause:

+      // return Conjunction(clauses.Select(c => extract(c)));

+      var conj = Conjunction(clauses);

+      return conj != null ? extract(conj) : conj;

     }

 

     private static Expr Conjunction(IEnumerable<Expr> conjuncts)

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);