Renamed NonNullElements to NonNullDictionaryAndValues because the keys to dictionaries are non-null, which is enforced by the implementation of Dictionary.

Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.

1 files changed, 2 insertions, 2 deletions

diff --git a/Source/Core/GraphAlgorithms.cs b/Source/Core/GraphAlgorithms.cs
index 0815e54a..a19cf96c 100644
--- a/Source/Core/GraphAlgorithms.cs
+++ b/Source/Core/GraphAlgorithms.cs
@@ -71,7 +71,7 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public sealed class StronglyConnectedComponents<Node> : IEnumerable<SCC<Node>/*!*/> {

+  public sealed class StronglyConnectedComponents<Node> : IEnumerable<SCC<Node>/*!*/> where Node : class {

     private readonly IDictionary<Node/*!*/, object>/*!*/ graph;

     [ContractInvariantMethod]

     void graphInvariantMethod() {

@@ -175,7 +175,7 @@ namespace Microsoft.Boogie {
     private readonly Stack<Node/*!*/>/*!*/ postOrder = new Stack<Node/*!*/>();

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(seen != null && cce.NonNullElements(seen.Keys));

+      Contract.Invariant(seen != null);

       Contract.Invariant(cce.NonNullElements(postOrder));

     }