Worked on the verification result caching.

1 files changed, 30 insertions, 2 deletions

diff --git a/Source/ExecutionEngine/VerificationResultCache.cs b/Source/ExecutionEngine/VerificationResultCache.cs
index e25c9306..bacdfaf8 100644
--- a/Source/ExecutionEngine/VerificationResultCache.cs
+++ b/Source/ExecutionEngine/VerificationResultCache.cs
@@ -324,6 +324,7 @@ namespace Microsoft.Boogie
   sealed class DependencyCollector : ReadOnlyVisitor

   {

     private DeclWithFormals currentDeclaration;

+    private Axiom currentAxiom;

 

     public static void Collect(Program program)

     {

@@ -389,6 +390,26 @@ namespace Microsoft.Boogie
       return result;

     }

 

+    public override Axiom VisitAxiom(Axiom node)

+    {

+      if (node.DependenciesCollected)

+      {

+        if (currentDeclaration != null && node.FunctionDependencies != null)

+        {

+          foreach (var f in node.FunctionDependencies)

+          {

+            currentDeclaration.AddFunctionDependency(f);

+          }

+        }

+        return node;

+      }

+      currentAxiom = node;

+      var result = base.VisitAxiom(node);

+      node.DependenciesCollected = true;

+      currentAxiom = null;

+      return result;

+    }

+

     public override Function VisitFunction(Function node)

     {

       currentDeclaration = node;

@@ -427,9 +448,16 @@ namespace Microsoft.Boogie
     public override Expr VisitNAryExpr(NAryExpr node)

     {

       var funCall = node.Fun as FunctionCall;

-      if (funCall != null && currentDeclaration != null)

+      if (funCall != null)

       {

-        currentDeclaration.AddFunctionDependency(funCall.Func);

+        if (currentDeclaration != null)

+        {

+          currentDeclaration.AddFunctionDependency(funCall.Func);

+        }

+        if (currentAxiom != null)

+        {

+          currentAxiom.AddFunctionDependency(funCall.Func);

+        }

       }

 

       return base.VisitNAryExpr(node);