fix

Author: stefan-aws

tests/Tests.dfy

@@ -81,7 +81,7 @@ module Tests {
     var k := Helper.Log2Floor(u);
     for i := 0 to n {
       var l := r.UniformPowerOfTwoSample(u);
-      expect 0 <= l < Helper.Power(2, k), "sample in the right bound";
+      expect 0 <= l < Helper.Power(2, k), "sample not in the right bound";
       if l in m.Keys {
         m := m[l := m[l] + 1];
       } else {
@@ -96,7 +96,7 @@ module Tests {
       var item :| item in items;
       items := items - {item};
       if item.0 < Helper.Power(2, k) {
-        testBernoulliIsWithin4SigmaOfTrueMean(n, item.1 as real, 1.0 / (u as real), "p(" + natToString(item.0) + ")");
+        testBernoulliIsWithin4SigmaOfTrueMean(n, item.1 as real, 1.0 /  (Helper.Power(2, k) as real), "p(" + natToString(item.0) + ")");
       }
     }
   }
@@ -110,7 +110,7 @@ module Tests {
     var m: map<nat,nat> := map[];
     for i := 0 to n {
       var l := r.UniformSample(u);
-      expect 0 <= l < u, "sample in the right bound";
+      expect 0 <= l < u, "sample not in the right bound";
       if l in m.Keys {
         m := m[l := m[l] + 1];
       } else {