diff options
| -rw-r--r-- | Dafny/Translator.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index 31e39af2..b486681b 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -4012,7 +4012,7 @@ namespace Microsoft.Dafny { TrStmt(h, b, locals, etran);
}
// NadiaTodo: add error messages
- b.Add(new Bpl.AssertCmd(s.Tok, etran.TrExpr(s.Steps[i])));
+ b.Add(Assert(s.Terms[i + 1].tok, etran.TrExpr(s.Steps[i]), "this calculation step might not hold"));
b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));
if (i == s.Steps.Count - 1) {
// first iteration (last step)
|