diff options
Diffstat (limited to 'Source/VCGeneration/OrderingAxioms.cs')
| -rw-r--r-- | Source/VCGeneration/OrderingAxioms.cs | 2 |
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));
|