From 6bcf55dc4d0158a1b06a3b9e1a245e1d13ff46d3 Mon Sep 17 00:00:00 2001
From: John Tristan <trjohnb@amazon.com>
Date: Thu, 29 Feb 2024 11:50:06 -0500
Subject: [PATCH] Improved loop for parameters of Bernoulli expneg greater than
 1 (#157)

By submitting this pull request, I confirm that my contribution is made
under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).
---
 src/DafnyVMCTrait.dfy | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/DafnyVMCTrait.dfy b/src/DafnyVMCTrait.dfy
index cf60dfd0..ab198d06 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 == true) {
+          o := B;
+        } else {
+          var R := BernoulliExpNegSampleGenLoop(iter - 1);
+          o := R;
+        }
       }
     }