diff options
| -rw-r--r-- | Source/Dafny/Translator.cs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 940bb328..1700198f 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -7040,6 +7040,7 @@ namespace Microsoft.Dafny { {
Contract.Requires(tok != null);
Contract.Requires(condition != null);
+ Contract.Ensures(Contract.Result<Bpl.Requires>() != null);
Bpl.Requires req = new Bpl.Requires(ForceCheckToken.Unwrap(tok), free, condition, comment);
if (errorMessage != null) {
req.ErrorData = errorMessage;
|