Update snapshot tests

verus-lang · Apr 9, 2024 · a1d084d · a1d084d
1 parent f7a7115
commit a1d084d
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 0 deletions.
diff --git a/examples/verus-snapshot/source/vstd/source/vstd/seq_lib.rs b/examples/verus-snapshot/source/vstd/source/vstd/seq_lib.rs
@@ -971,6 +971,7 @@ impl<A> Seq<Seq<A>> {
             self.len() == 1 ==> self.flatten() == self.first(),
     {
         broadcast use Seq::add_empty_right;
+
         if self.len() == 1 {
             assert(self.flatten() =~= self.first().add(self.drop_first().flatten()));
         }
@@ -1022,6 +1023,7 @@ impl<A> Seq<Seq<A>> {
         decreases self.len(),
     {
         broadcast use Seq::add_empty_right, Seq::push_distributes_over_add;
+
         if self.len() != 0 {
             self.drop_last().lemma_flatten_and_flatten_alt_are_equivalent();
             seq![self.last()].lemma_flatten_one_element();

diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs
@@ -1990,6 +1990,7 @@ mod m4 {
                 p.inv(),
         {
             broadcast use Ring::properties;
+
             assert(p.spec_succ().spec_prev() == p);
             assert(p.spec_prev().spec_succ() == p);
         }