Make caching of verification results more fine-grained for changes that affect preconditions.

1 files changed, 23 insertions, 0 deletions

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index f3a943b8..c19140d7 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -467,6 +467,29 @@ namespace Microsoft.Boogie {
         var mid = (start + end) / 2;

         return Expr.And(BinaryTreeAnd(terms, start, mid), BinaryTreeAnd(terms, mid + 1, end));

     }

+

+    public static Expr And(IEnumerable<Expr> conjuncts, bool returnNullIfEmpty = false)

+    {

+      Expr result = null;

+      foreach (var c in conjuncts)

+      {

+        if (result != null)

+        {

+          result = LiteralExpr.And(result, c);

+          result.Type = Type.Bool;

+        }

+        else

+        {

+          result = c;

+          result.Type = Type.Bool;

+        }

+      }

+      if (result == null && !returnNullIfEmpty)

+      {

+        result = Expr.True;

+      }

+      return result;

+    }

   }

   [ContractClassFor(typeof(Expr))]

   public abstract class ExprContracts : Expr {