diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-01-10 20:14:42 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-01-10 20:14:42 -0800 |
| commit | 20bbf073f2dd3801933c484b5670be164ebd4015 (patch) | |
| tree | 294f016204bfa8523429a58ed266fb7a4de487d8 /Dafny/Translator.cs | |
| parent | ba9ff7d99f6020cd684551e04bb746c2a89ce443 (diff) | |
Dafny: fixed bugs in contract types, and a code bug that caused a contract to fail
Diffstat (limited to 'Dafny/Translator.cs')
| -rw-r--r-- | Dafny/Translator.cs | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index 27880f9d..0e928e4e 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -3114,7 +3114,7 @@ namespace Microsoft.Dafny { Contract.Requires(tok != null);
Contract.Requires(condition != null);
Contract.Requires(errorMessage != null);
- Contract.Ensures(Contract.Result<Bpl.AssertCmd>() != null);
+ Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);
if (RefinementToken.IsInherited(tok, currentModule)) {
// produce an assume instead
@@ -3131,7 +3131,7 @@ namespace Microsoft.Dafny { Contract.Requires(tok != null);
Contract.Requires(errorMessage != null);
Contract.Requires(condition != null);
- Contract.Ensures(Contract.Result<Bpl.AssertCmd>() != null);
+ Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);
if (RefinementToken.IsInherited(tok, currentModule)) {
// produce a "skip" instead
@@ -3150,7 +3150,7 @@ namespace Microsoft.Dafny { Contract.Requires(tok != null);
Contract.Requires(errorMessage != null);
Contract.Requires(condition != null);
- Contract.Ensures(Contract.Result<Bpl.AssertCmd>() != null);
+ Contract.Ensures(Contract.Result<Bpl.PredicateCmd>() != null);
if (RefinementToken.IsInherited(tok, currentModule)) {
// produce an assume instead
|