Update unwinding tutorial (rust-lang#1877)

Co-authored-by: Adrian Palacios <[email protected]>

Author: zhassan-aws

docs/src/tutorial-loop-unwinding.md

@@ -60,10 +60,9 @@ The code tries to execute more than 1 loop iteration.
 <summary>Click to see explanation for the exercise</summary>
 
 Since the proof harness is trying to limit the array to size 10, an initial unwind value of 10 seems like the obvious place to start.
-But that's not large enough for Kani.
+But that's not large enough for Kani, and we still see the "unwinding assertion" failure.
 
-At size 11, we still see the "unwinding assertion" failure, but now we can see the actual failures we're trying to find, too.
-Finally at size 12, the "unwinding assertion" goes away, just leaving the other failures.
+At size 11, the "unwinding assertion" goes away, and now we can see the actual failure we're trying to find too.
 We'll explain why we see this behavior in a moment.
 
 </details>
@@ -72,25 +71,20 @@ Once we have increased the unwinding limit high enough, we're left with these fa
 
 ```
 SUMMARY:
- ** 2 of 67 failed
+ ** 1 of 68 failed
 Failed Checks: index out of bounds: the length is less than or equal to the given index
  File: "./src/lib.rs", line 12, in initialize_prefix
-Failed Checks: dereference failure: pointer outside object bounds
- File: "./src/lib.rs", line 12, in initialize_prefix
 
 VERIFICATION:- FAILED
 ```
 
 **Exercise**: Fix the off-by-one error, and get the (bounded) proof to go through.
 
-We now return to the question: why is 12 the unwinding bound?
-Well, the first answer is: it isn't!
-Reduce it to 11 and observe that the proof now still works!
+We now return to the question: why is 11 the unwinding bound?
 
 Kani needs the unwinding bound to be "one more than" the number of loop iterations.
 We previously had an off-by-one error that tried to do 11 iterations on an array of size 10.
-So... the unwinding bound needed to be 12, then.
-Fixing that error to do the correct 10 iterations means we can now successfully reduce that unwind bound to 11 again.
+So... the unwinding bound needed to be 11, then.
 
 > **NOTE**: Presently, there are some situations where "number of iterations of a loop" can be less obvious than it seems.
 > This can be easily triggered with use of `break` or `continue` within loops.
@@ -115,7 +109,7 @@ In that case you can either use `--default-unwind x` to set an unwind bound for
 Or you can _override_ a harness's bound, but only when running a specific harness:
 
 ```
-cargo kani --harness check_initialize_prefix --unwind 12
+cargo kani --harness check_initialize_prefix --unwind 11
 ```
 
 Finally, you might be interested in defaulting the unwind bound to 1, to force termination (and force supplying a bound) on all your proof harnesses.