diff options
-rw-r--r-- | Source/Houdini/ConcurrentHoudini.cs | 13 |
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); |