small fix in the parallel refutation sharing

1 files changed, 10 insertions, 3 deletions

diff --git a/Source/Houdini/ConcurrentHoudini.cs b/Source/Houdini/ConcurrentHoudini.cs
index b16370e9..b92cb7bc 100644
--- a/Source/Houdini/ConcurrentHoudini.cs
+++ b/Source/Houdini/ConcurrentHoudini.cs
@@ -206,12 +206,20 @@ namespace Microsoft.Boogie.Houdini
 
       currentHoudiniState = new HoudiniState(BuildWorkList(program), BuildAssignment(houdiniConstants));
 
-      if(initialAssignment != null) {
-        foreach(var v in currentHoudiniState.Assignment.Keys.ToList()) {
+      if (initialAssignment != null) {
+        foreach (var v in currentHoudiniState.Assignment.Keys.ToList()) {
           currentHoudiniState.Assignment[v] = initialAssignment[v.Name];
         }
       }
 
+      if (refutedSharedAnnotations.Count > 0) {
+        foreach (var v in currentHoudiniState.Assignment.Keys.ToList()) {
+          if (refutedSharedAnnotations.ContainsKey(v.Name)) {
+            currentHoudiniState.Assignment[v] = false;
+          }
+        }
+      }
+
       foreach (Implementation impl in vcgenFailures) {
         currentHoudiniState.addToBlackList(impl.Name);
       }
@@ -219,7 +227,6 @@ namespace Microsoft.Boogie.Houdini
       while (currentHoudiniState.WorkQueue.Count > 0) {
         this.NotifyIteration();
 
-        ExchangeRefutedAnnotations();
         currentHoudiniState.Implementation = currentHoudiniState.WorkQueue.Peek();
         this.NotifyImplementation(currentHoudiniState.Implementation);