1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy
index 505d9b74..3025cc00 100644
--- a/Test/dafny0/Modules1.dfy
+++ b/Test/dafny0/Modules1.dfy
@@ -125,11 +125,11 @@ abstract module Regression {
     predicate p<c,d>(m: map<c,d>)
 
     lemma m<a,b>(m: map<a,b>)
-      ensures exists m :: p(var m : map<a,b> := m; m);
+      ensures exists m {:nowarn} :: p(var m : map<a,b> := m; m) // WISH: Zeta-expanding the let binding would provide a good trigger
   }
 
   abstract module B
   {
-    import X as A
+    import X : A
   }
 }