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/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index aa0be9dd..91e33ea9 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -332,7 +332,7 @@ namespace Microsoft.Boogie
     static PipelineOutcome BoogiePipelineWithRerun (Program/*!*/ program, string/*!*/ bplFileName,

         out int errorCount, out int verified, out int inconclusives, out int timeOuts, out int outOfMemories)

     {Contract.Requires(program != null);

-    Contract.Requires(cce.NonNullElements(bplFileName));

+    Contract.Requires(bplFileName != null);

       Contract.Ensures(0 <= Contract.ValueAtReturn(out inconclusives) && 0 <= Contract.ValueAtReturn(out timeOuts));