diff options
| author |  Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2012-09-19 14:05:03 +0200 |
|---|---|---|
| committer | Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2012-09-19 14:05:03 +0200 |
| commit | 8264fd48ce81180c78fa3f9c76ed31c52723017b (patch) | |
| tree | adfcdb12fe8089024796ca42a0490cf36290733b /Source/Dafny | |
| parent | 1f91d2e97ef23a5182d0db8fdfbe4716fec46dd2 (diff) | |
Made verification error message more explicit
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/Translator.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 675e62e8..531bb51a 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -4012,7 +4012,7 @@ namespace Microsoft.Dafny { if (h != null) {
TrStmt(h, b, locals, etran);
}
- b.Add(Assert(s.Lines[i + 1].tok, etran.TrExpr(s.Steps[i]), "this calculation step might not hold"));
+ b.Add(Assert(s.Lines[i + 1].tok, etran.TrExpr(s.Steps[i]), "the calculation step between the previous line and this line might not hold"));
b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));
if (i == s.Steps.Count - 1) {
// first iteration (last step)
|