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, 1 insertions, 1 deletions

diff --git a/Source/VCGeneration/OrderingAxioms.cs b/Source/VCGeneration/OrderingAxioms.cs
index 877fba13..4fbc80da 100644
--- a/Source/VCGeneration/OrderingAxioms.cs
+++ b/Source/VCGeneration/OrderingAxioms.cs
@@ -24,7 +24,7 @@ namespace Microsoft.Boogie {
     void ObjectInvariant() {

       Contract.Invariant(Gen != null);

       Contract.Invariant(Translator != null);

-      Contract.Invariant(cce.NonNullElements(OneStepFuns));

+      Contract.Invariant(cce.NonNullDictionaryAndValues(OneStepFuns));

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

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

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