diff options
Diffstat (limited to 'Source/Dafny/Cloner.cs')
| -rw-r--r-- | Source/Dafny/Cloner.cs | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index dd2eed69..032e30a0 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -550,13 +550,21 @@ namespace Microsoft.Dafny r = new ForallStmt(Tok(s.Tok), Tok(s.EndTok), s.BoundVars.ConvertAll(CloneBoundVar), null, CloneExpr(s.Range), s.Ens.ConvertAll(CloneMayBeFreeExpr), CloneStmt(s.Body));
} else if (stmt is CalcStmt) {
- var s = (CalcStmt)stmt;
- r = new CalcStmt(Tok(s.Tok), Tok(s.EndTok), CloneCalcOp(s.Op), s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneBlockStmt), s.StepOps.ConvertAll(CloneCalcOp), CloneCalcOp(s.ResultOp), CloneAttributes(s.Attributes));
+ var s = (CalcStmt)stmt;
+ // calc statements have the unusual property that the last line is duplicated. If that is the case (which
+ // we expect it to be here), we share the clone of that line as well.
+ var lineCount = s.Lines.Count;
+ var lines = new List<Expression>(lineCount);
+ for (int i = 0; i < lineCount; i++) {
+ lines.Add(i == lineCount - 1 && 2 <= lineCount && s.Lines[i] == s.Lines[i - 1] ? lines[i - 1] : CloneExpr(s.Lines[i]));
+ }
+ Contract.Assert(lines.Count == lineCount);
+ r = new CalcStmt(Tok(s.Tok), Tok(s.EndTok), CloneCalcOp(s.Op), lines, s.Hints.ConvertAll(CloneBlockStmt), s.StepOps.ConvertAll(CloneCalcOp), CloneCalcOp(s.ResultOp), CloneAttributes(s.Attributes));
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
r = new MatchStmt(Tok(s.Tok), Tok(s.EndTok), CloneExpr(s.Source),
- s.Cases.ConvertAll(CloneMatchCaseStmt), s.UsesOptionalBraces);
+ s.Cases.ConvertAll(CloneMatchCaseStmt), s.UsesOptionalBraces);
} else if (stmt is AssignSuchThatStmt) {
var s = (AssignSuchThatStmt)stmt;
|