diff options
| author |  Jason Koenig <unknown> | 2012-07-13 17:50:18 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2012-07-13 17:50:18 -0700 |
| commit | 5359210b793fd9ba25027e6ca882735c01e370bf (patch) | |
| tree | 8dc795417830e5fab5191525ba420bd51dbe8f3a /Source | |
| parent | c71f8edce17944b5198ac968da17c19c96b39877 (diff) | |
Dafny: update statements match up correctly in skeletons.
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/RefinementTransformer.cs | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 18f7cc61..30fac1cc 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -1476,6 +1476,12 @@ namespace Microsoft.Dafny { } else if (other is BlockStmt && ((BlockStmt)other).Labels == null) {
return true; // both are unlabeled
}
+ } else if (nxt is UpdateStmt) {
+ var up = (UpdateStmt)nxt;
+ if (other is AssignSuchThatStmt) {
+ var oth = other as AssignSuchThatStmt;
+ return oth != null && LeftHandSidesAgree(oth.Lhss, up.Lhss);
+ }
}
// not a potential match
|