Reduce resource usage

dafny-lang · Nov 3, 2023 · 44f2af5 · 44f2af5
1 parent 671d977
commit 44f2af5
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/src/Distributions/BernoulliExpNeg/Implementation.dfy b/src/Distributions/BernoulliExpNeg/Implementation.dfy
@@ -29,8 +29,11 @@ module BernoulliExpNeg.Implementation {
         invariant gamma'.numer >= 0
         invariant Model.GammaReductionLoop((true, gamma))(old(s)) == Model.GammaReductionLoop((b, gamma'))(s)
       {
+        var prevGamma := gamma';
+        var prevS := s;
         b := BernoulliExpNegSampleCaseLe1(Rationals.Int(1));
         gamma' := Rationals.Rational(gamma'.numer - gamma'.denom, gamma'.denom);
+        assert Model.GammaReductionLoop((true, prevGamma))(prevS) == Model.GammaReductionLoop((b, gamma'))(s);
       }
       if b {
         c:= BernoulliExpNegSampleCaseLe1(gamma');