Fix issue 104. Use ResolvedExpression to compute subexpressions for

DatatypeUpdateExpr if ResovedExpression is not null.

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;

+          }

         }

       }

     }