summaryrefslogtreecommitdiff
path: root/Source/Dafny/Dafny.atg
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Dafny/Dafny.atg')
-rw-r--r--Source/Dafny/Dafny.atg3
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index dcc9a3ca..bc972495 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -437,7 +437,8 @@ IteratorDecl<ModuleDefinition module, out IteratorDecl/*!*/ iter>
[ BlockStmt<out body, out bodyStart, out bodyEnd>
]
(. iter = new IteratorDecl(id, id.val, module, typeArgs, ins, outs,
- new Specification<FrameExpression>(mod, modAttrs), new Specification<FrameExpression>(reads, readsAttrs),
+ new Specification<FrameExpression>(reads, readsAttrs),
+ new Specification<FrameExpression>(mod, modAttrs),
new Specification<Expression>(decreases, decrAttrs),
req, ens, yieldReq, yieldEns,
body, attrs, signatureOmitted);