diff options
| -rw-r--r-- | Dafny/Translator.cs | 12 | ||||
| -rw-r--r-- | Test/dafny2/Calculations.dfy | 5 |
2 files changed, 12 insertions, 5 deletions
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index 2e486533..ccc9ff4f 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -4009,7 +4009,17 @@ namespace Microsoft.Dafny { for (int i = s.Steps.Count; 0 <= --i; ) {
b = new Bpl.StmtListBuilder();
TrStmt(s.Hints[i], b, locals, etran);
- 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"));
+ bool splitHappened;
+ var ss = TrSplitExpr(s.Steps[i], etran, out splitHappened);
+ if (!splitHappened) {
+ b.Add(AssertNS(s.Lines[i + 1].tok, etran.TrExpr(s.Steps[i]), "the calculation step between the previous line and this line might not hold"));
+ } else {
+ foreach (var split in ss) {
+ if (!split.IsFree) {
+ b.Add(AssertNS(s.Lines[i + 1].tok, split.E, "the calculation step between the previous line and this line might not hold"));
+ }
+ }
+ }
b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));
ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, null);
}
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy index 1ddd8603..8c13457b 100644 --- a/Test/dafny2/Calculations.dfy +++ b/Test/dafny2/Calculations.dfy @@ -80,10 +80,7 @@ ghost method Lemma_Revacc_calc(xs: List, ys: List) concat(revacc(xrest, Cons(x, Nil)), ys);
{ Lemma_RevCatCommute(); } // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)
revacc(xrest, concat(Cons(x, Nil), ys));
- {
- assert forall g, gs :: concat(Cons(g, Nil), gs) == Cons(g, gs);
- assert concat(Cons(x, Nil), ys) == Cons(x, ys);
- }
+ // def. concat (x2)
revacc(xrest, Cons(x, ys));
// def. revacc
revacc(xs, ys);
|