fixes

Author: stefan-aws

scripts/test.sh

@@ -21,7 +21,7 @@ time $DAFNY test --target:$TARGET_LANG src/interop/$TARGET_LANG/Extern/Random.$T
 echo Running $TARGET_LANG documentation...
 
 echo "Building docs/dafny/ExamplesRandom.dfy..." 
-$DAFNY build docs/dafny/ExamplesRandom.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/Extern/Random.$TARGET_LANG src/DafnyVMC.dfy src/DafnyVMCTrait.dfy  dfyconfig.toml --no-verify
+$DAFNY build docs/dafny/ExamplesRandom.dfy --target:$TARGET_LANG src/interop/$TARGET_LANG/Extern/Random.$TARGET_LANG src/DafnyVMC.dfy src/DafnyVMCTrait.dfy dfyconfig.toml --no-verify
 echo "Executing compiled docs/dafny/ExamplesRandom.dfy:" 
 if [ "$TARGET_LANG" = "java" ]
 then

scripts/verify.sh

@@ -9,4 +9,4 @@ then
 fi
 
 echo Verifying the proofs...
-time $DAFNY verify dfyconfig.toml docs/dafny/ExamplesRandom.dfy tests/Tests.dfy tests/TestsRandom.dfy --resource-limit 20000 # 20M resource usage
+time $DAFNY verify dfyconfig.toml docs/dafny/ExamplesRandom.dfy tests/Tests.dfy tests/TestsRandom.dfy src/DafnyVMC.dfy src/DafnyVMCTrait.dfy --resource-limit 20000 # 20M resource usage

src/Distributions/Coin/Implementation.dfy

@@ -16,9 +16,10 @@ module Coin.Implementation {
       ensures Model.Sample(old(s)) == Monad.Result(b, s)
     {
       var x := UniformPowerOfTwoSample(2);
-      b := if x == 0 then false else true;
+      b := if x == 1 then true else false;
+      reveal UniformPowerOfTwo.Model.Sample();    
     }
-
+    
   }
 
 }