summaryrefslogtreecommitdiff
path: root/Source/DafnyExtension/ResolverTagger.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/DafnyExtension/ResolverTagger.cs')
-rw-r--r--Source/DafnyExtension/ResolverTagger.cs2
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index d1af6878..ca9ed169 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -311,7 +311,7 @@ namespace DafnyLanguage
Snapshot = snapshot;
}
public SnapshotSpan Span() {
- Contract.Requires(Snapshot != null); // requires that Snapshot has been filled in
+ Contract.Assume(Snapshot != null); // requires that Snapshot has been filled in
var line = Snapshot.GetLineFromLineNumber(Line);
Contract.Assume(Column <= line.Length); // this is really a precondition of the constructor + FillInSnapshot
var length = Math.Min(line.Length - Column, 5);