From 9f4d81cb7056501547a5116796a3112da8054433 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Mon, 29 Feb 2016 15:31:30 -0800
Subject: Added a return-value contract

---
 Source/Dafny/Translator.cs | 1 +
 1 file changed, 1 insertion(+)

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;
-- 
cgit v1.2.3