remove split on every assert

src/Distributions/Uniform/Interface.dfy

@@ -40,12 +40,13 @@ module Uniform.Interface {
       ensures u < n
       ensures Model.Sample(n as nat)(old(s)) == Monad.Result(u as nat, s)
 
-    method UniformIntervalSample32(a: int32, b: int32) returns (u: int32)
+    method UniformIntervalSample32<T>(a: int32, b: int32, ghost arr: array<T>) returns (u: int32)
       modifies `s
       decreases *
       requires 0 < b as int - a as int < 0x8000_0000
       ensures a <= u < b
       ensures Model.IntervalSample(a as int, b as int)(old(s)) == Monad.Result(u as int, s)
+      ensures old(arr[..]) == arr[..]
     {
       var v := UniformSample32(b-a);
       assert Model.Sample(b as int - a as int)(old(s)) == Monad.Result(v as nat, s);

src/Util/FisherYates/Implementation.dfy

@@ -13,7 +13,7 @@ module FisherYates.Implementation {
 
   trait {:termination false} Trait extends Interface.Trait {
 
-    method {:vcs_split_on_every_assert} Shuffle<T>(a: array<T>)
+    method Shuffle<T>(a: array<T>)
       decreases *
       modifies `s, a
       requires a.Length < 0x8000_0000
@@ -26,9 +26,10 @@ module FisherYates.Implementation {
           invariant Equivalence.LoopInvariant(prevI, i, a, prevASeq, old(a[..]), old(s), prevS, s) // ghost
         {
           prevI, prevASeq, prevS := i, a[..], s; // ghost
-          var j := UniformIntervalSample32(i, a.Length as nat32);
+          var j := UniformIntervalSample32(i, a.Length as nat32, a);
           assert prevASeq == a[..]; // ghost
           Swap(a, i, j);
+          assert Equivalence.LoopInvariant(prevI, i+1, a, prevASeq, old(a[..]), old(s), prevS, s); // ghost
         }
       } else {
         Equivalence.ShuffleElseClause(a, old(a[..]), old(s), s); // ghost