1 files changed, 9 insertions, 5 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 99cf791f..dc925519 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -1660,20 +1660,24 @@ namespace Microsoft.Dafny {
   {
     public readonly List<MaybeFreeExpression/*!*/>/*!*/ Invariants;
     public readonly List<Expression/*!*/>/*!*/ Decreases;
+    public readonly List<FrameExpression/*!*/>/*!*/ Mod;
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(cce.NonNullElements(Invariants));
       Contract.Invariant(cce.NonNullElements(Decreases));
+      Contract.Invariant(cce.NonNullElements(Mod));
     }
-    public LoopStmt(IToken tok, List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases)
+    public LoopStmt(IToken tok, List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod)
     : base(tok) 
     {
       Contract.Requires(tok != null);
       Contract.Requires(cce.NonNullElements(invariants));
       Contract.Requires(cce.NonNullElements(decreases));
+      Contract.Requires(cce.NonNullElements(mod));
 
       this.Invariants = invariants;
       this.Decreases = decreases;
+      this.Mod = mod;
     }
   }
 
@@ -1687,9 +1691,9 @@ namespace Microsoft.Dafny {
     }
 
     public WhileStmt(IToken tok, Expression guard,
-                     List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases,
+                     List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod,
                      Statement/*!*/ body)
-      : base(tok, invariants, decreases) {
+      : base(tok, invariants, decreases, mod) {
       Contract.Requires(tok != null);
       Contract.Requires(body != null);
       this.Guard = guard;
@@ -1705,9 +1709,9 @@ namespace Microsoft.Dafny {
       Contract.Invariant(Alternatives != null);
     }
     public AlternativeLoopStmt(IToken tok,
-                               List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases,
+                               List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod,
                                List<GuardedAlternative> alternatives)
-      : base(tok, invariants, decreases) {
+      : base(tok, invariants, decreases, mod) {
       Contract.Requires(tok != null);
       Contract.Requires(alternatives != null);
       this.Alternatives = alternatives;