From d3c778854c2dc792a2dfbd9c5b05d667d18fb4c4 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
Date: Wed, 4 Nov 2015 16:27:42 -0800
Subject: Fix issue 104. Use ResolvedExpression to compute subexpressions for
 DatatypeUpdateExpr if ResovedExpression is not null.

---
 Source/Dafny/DafnyAst.cs | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

(limited to 'Source/Dafny')

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;
+          }
         }
       }
     }
-- 
cgit v1.2.3