summaryrefslogtreecommitdiff
path: root/Source/Dafny
diff options
context:
space:
mode:
authorGravatar qunyanm <unknown>2015-11-04 16:27:42 -0800
committerGravatar qunyanm <unknown>2015-11-04 16:27:42 -0800
commitd3c778854c2dc792a2dfbd9c5b05d667d18fb4c4 (patch)
tree7c5c0554b13c19256b8bb8863188797f9ca047dc /Source/Dafny
parent2b7d31bb3e0276028a8bc50c4933ea60fed5fb60 (diff)
Fix issue 104. Use ResolvedExpression to compute subexpressions for
DatatypeUpdateExpr if ResovedExpression is not null.
Diffstat (limited to 'Source/Dafny')
-rw-r--r--Source/Dafny/DafnyAst.cs12
1 files changed, 9 insertions, 3 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 16b29c2b..fdbd484e 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -7800,9 +7800,15 @@ namespace Microsoft.Dafny {
public override IEnumerable<Expression> SubExpressions {
get {
- yield return Root;
- foreach (var update in Updates) {
- yield return update.Item3;
+ if (ResolvedExpression == null) {
+ yield return Root;
+ foreach (var update in Updates) {
+ yield return update.Item3;
+ }
+ } else {
+ foreach (var e in ResolvedExpression.SubExpressions) {
+ yield return e;
+ }
}
}
}