Added a return-value contract

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;