Dafny: fixed some test cases

1 files changed, 6 insertions, 4 deletions

diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy
index 146129b5..8857482f 100644
--- a/Test/dafny0/Predicates.dfy
+++ b/Test/dafny0/Predicates.dfy
@@ -78,9 +78,10 @@ module Tight refines Loose {
   }

 }

 

-module UnawareClient imports Loose {

+module UnawareClient {

+  module L = Loose;

   method Main0() {

-    var n := new MyNumber.Init();

+    var n := new L.MyNumber.Init();

     assert n.N == 0;  // error: this is not known

     n.Inc();

     n.Inc();

@@ -89,9 +90,10 @@ module UnawareClient imports Loose {
   }

 }

 

-module AwareClient imports Tight {

+module AwareClient {

+  module T = Tight;

   method Main1() {

-    var n := new MyNumber.Init();

+    var n := new T.MyNumber.Init();

     assert n.N == 0;

     n.Inc();

     n.Inc();