From 2151f863ce418b3deb50c9a8d955f4b3b72cead6 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Tue, 16 Sep 2014 12:43:10 -0700
Subject: fixed a crash

---
 Source/Houdini/Houdini.cs | 25 +++++++++++++++----------
 1 file changed, 15 insertions(+), 10 deletions(-)

(limited to 'Source/Houdini')

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index af1bd8ad..7dfa1bc7 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -944,18 +944,22 @@ namespace Microsoft.Boogie.Houdini {
       List<Implementation> implementations = new List<Implementation>();
       switch (refutedAnnotation.Kind) {
         case RefutedAnnotationKind.REQUIRES:
-          foreach (Implementation callee in callGraph.Successors(currentImplementation)) {
-            houdiniSessions.TryGetValue(callee, out session);
-            Contract.Assume(callee.Proc != null);
-            if (callee.Proc.Equals(refutedAnnotation.CalleeProc) && session.InUnsatCore(refutedAnnotation.Constant)) 
-              implementations.Add(callee);
-          }
+              foreach (Implementation callee in callGraph.Successors(currentImplementation))
+              {
+                  if (vcgenFailures.Contains(callee)) continue;
+                  houdiniSessions.TryGetValue(callee, out session);
+                  Contract.Assume(callee.Proc != null);
+                  if (callee.Proc.Equals(refutedAnnotation.CalleeProc) && session.InUnsatCore(refutedAnnotation.Constant))
+                      implementations.Add(callee);
+              }
           break;
         case RefutedAnnotationKind.ENSURES:
-          foreach (Implementation caller in callGraph.Predecessors(currentImplementation)) {
-            houdiniSessions.TryGetValue(caller, out session);
-            if (session.InUnsatCore(refutedAnnotation.Constant))
-              implementations.Add(caller);
+          foreach (Implementation caller in callGraph.Predecessors(currentImplementation))
+          {
+              if (vcgenFailures.Contains(caller)) continue;
+              houdiniSessions.TryGetValue(caller, out session);
+              if (session.InUnsatCore(refutedAnnotation.Constant))
+                  implementations.Add(caller);
           }
           break;
         case RefutedAnnotationKind.ASSERT: //the implementation is already in queue
@@ -963,6 +967,7 @@ namespace Microsoft.Boogie.Houdini {
           {
               foreach (var impl in crossDependencies.assumedInImpl[refutedAnnotation.Constant.Name])
               {
+                  if (vcgenFailures.Contains(impl)) continue;
                   houdiniSessions.TryGetValue(impl, out session);
                   if (session.InUnsatCore(refutedAnnotation.Constant))
                       implementations.Add(impl);
-- 
cgit v1.2.3