1
00:00:00,000 --> 00:00:08,000
The body of the While loop contains an Assume statement. 

2
00:00:09,000 --> 00:00:20,000
We apply the "WhileStrInv" tactic to strengthen the invariant.

3
00:00:22,000 --> 00:00:30,000
An unknown program fragment is added inside the while loop to preserve the added invariant.

4
00:00:32,000 --> 00:00:38,000
An "Assume" statement is introduced before the while loop to establish the added invariant at the entry of the while loop.