diff options
author | mikebarnett <unknown> | 2011-03-10 17:37:58 +0000 |
---|---|---|
committer | mikebarnett <unknown> | 2011-03-10 17:37:58 +0000 |
commit | 768ee8abb31d912cfdc8eeaf41d7f44f1691ce0c (patch) | |
tree | 533ab6aa0d91c5a5e7c66125834fb5b8695ccf71 /Source/Provers/Z3/Prover.cs | |
parent | e28c62b12194be07e3ecb3301e6b3e0336bcac2a (diff) |
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.
Diffstat (limited to 'Source/Provers/Z3/Prover.cs')
-rw-r--r-- | Source/Provers/Z3/Prover.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs index c2bb7500..83294381 100644 --- a/Source/Provers/Z3/Prover.cs +++ b/Source/Provers/Z3/Prover.cs @@ -456,7 +456,7 @@ namespace Microsoft.Boogie.Z3 {
Contract.Requires(partitionToValue != null);
Contract.Requires(valueToPartition != null);
- Contract.Requires(cce.NonNullElements(identifierToPartition));
+ Contract.Requires(identifierToPartition != null);
Contract.Requires(cce.NonNullElements(partitionToIdentifiers));
Contract.Requires(cce.Owner.Same(cce.Owner.ElementProxy(partitionToValue), cce.Owner.ElementProxy(valueToPartition)));
string s = FromReadLine();
@@ -511,7 +511,7 @@ namespace Microsoft.Boogie.Z3 } else if (s[j] == '{') {
// array
List<List<int>/*!*/> arrayModel = new List<List<int>/*!*/>();
- Contract.Assert(Contract.ForAll(arrayModel, a => cce.NonNullElements(a)));
+ Contract.Assert(Contract.ForAll(arrayModel, a => a != null));
string array = s.Substring(j + 1);
int index1, index2;
string from, to;
|