From b3be45591fba0c3ddf0c87f5bb19287ea66cb95a Mon Sep 17 00:00:00 2001 From: stefan-aws Date: Thu, 29 Feb 2024 16:08:38 +0000 Subject: [PATCH] skeleton --- docs/java/BuildTest.java | 4 ++-- docs/py/BuildTest.py | 4 ++-- src/DafnyVMCTrait.dfy | 8 ++++++-- 3 files changed, 10 insertions(+), 6 deletions(-) diff --git a/docs/java/BuildTest.java b/docs/java/BuildTest.java index 2c64a04d..ea716ef0 100644 --- a/docs/java/BuildTest.java +++ b/docs/java/BuildTest.java @@ -13,8 +13,8 @@ public static void main(String[] args) { boolean[] arr5 = {true, false, false, true}; long[] arr6 = {111111L, 333333L, 999999L}; short[] arr7 = {-3, 0, 3}; - BigInteger num = BigInteger.valueOf(3); - BigInteger den = BigInteger.valueOf(5); + BigInteger num = BigInteger.valueOf(1); + BigInteger den = BigInteger.valueOf(1000); /* STANDARD RNG */ System.out.println("\nSTANDARD RNG TESTS\n"); diff --git a/docs/py/BuildTest.py b/docs/py/BuildTest.py index 0d9ee953..54a7db0b 100644 --- a/docs/py/BuildTest.py +++ b/docs/py/BuildTest.py @@ -6,8 +6,8 @@ def main(): arr3 = ["aa", "bb", "cc"] arr4 = ['a', 'b', 'c'] arr5 = [True, False, False, True] - num = 3 - den = 5 + num = 1 + den = 1000 # STANDARD RNG print("\nSTANDARD RNG TESTS\n") diff --git a/src/DafnyVMCTrait.dfy b/src/DafnyVMCTrait.dfy index cf60dfd0..4e516db1 100644 --- a/src/DafnyVMCTrait.dfy +++ b/src/DafnyVMCTrait.dfy @@ -83,8 +83,12 @@ module DafnyVMCTrait { o := true; } else { var B := BernoulliExpNegSampleUnit(1, 1); - var R := BernoulliExpNegSampleGenLoop(iter - 1); - o := B == true && R == true; + if B == false { + o := false; + } else { + var R := BernoulliExpNegSampleGenLoop(iter - 1); + o := R; + } } }