Merge branch 'main' into full-testing

stefan-aws · web-flow · commit ab58c82fbdad · 2024-02-29T18:08:48.000Z
diff --git 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;
+        }
       }
     }
 

Original file line number	Diff line number	Diff line change
`@@ -83,8 +83,12 @@ module DafnyVMCTrait {`
`83`	`83`	`o := true;`
`84`	`84`	`} else {`
`85`	`85`	`var B := BernoulliExpNegSampleUnit(1, 1);`
`86`		`- var R := BernoulliExpNegSampleGenLoop(iter - 1);`
`87`		`- o := B == true && R == true;`
	`86`	`+ if ! (B == true) {`
	`87`	`+ o := B;`
	`88`	`+ } else {`
	`89`	`+ var R := BernoulliExpNegSampleGenLoop(iter - 1);`
	`90`	`+ o := R;`
	`91`	`+ }`
`88`	`92`	`}`
`89`	`93`	`}`
`90`	`94`