@@ -4,17 +4,17 @@ expression: output
44-- -
55exiting with verification errors
66error : prover ::ensures does not hold
7- ┌─ tests / inputs / loop_invariant / issue - 416.move :12 :1
8- │
9- 12 │ ╭ fun bar_loop_inv (i : u64 , stop : u64 , v__3 : & vector <u8 >, v: & vector<u8 >, r: & vector<u8 >): bool {
10- 13 │ │ i <= stop && v__3 .length () == stop - i && r == map_range ! (v , 0 , i , | x | flip (x ))
11- 14 │ │ && ! exists ! (| j | more_loop_inv_3 (* j , v , v__3 ))
12- 15 │ │ }
13- │ ╰─^
14- │
15- ┌─ /NORMALIZED_HOME/.move/https___github_com_asymptotic-code_sui_git_NORMALIZED/crates/sui-framework/packages/move-stdlib/sources/macros.move:86 :12
16- │
17- 86 │ while (i < stop) {
18- │ - loop invariant is not preserved by the loop body
19- │
20- = at tests / inputs / loop_invariant / issue - 416.move :22 : bar_spec
7+ ┌─ tests / inputs / loop_invariant / issue - 416.move :12 :1
8+ │
9+ 12 │ ╭ fun bar_loop_inv (i : u64 , stop : u64 , v__3 : & vector <u8 >, v: & vector<u8 >, r: & vector<u8 >): bool {
10+ 13 │ │ i <= stop && v__3 .length () == stop - i && r == map_range ! (v , 0 , i , | x | flip (x ))
11+ 14 │ │ && ! exists ! (| j | more_loop_inv_3 (* j , v , v__3 ))
12+ 15 │ │ }
13+ │ ╰─^
14+ │
15+ ┌─ /NORMALIZED_HOME/.move/https___github_com_asymptotic-code_sui_git_NORMALIZED/crates/sui-framework/packages/move-stdlib/sources/macros.move:180 :12
16+ │
17+ 180 │ while (i < stop) {
18+ │ - loop invariant is not preserved by the loop body
19+ │
20+ = at tests / inputs / loop_invariant / issue - 416.move :22 : bar_spec
0 commit comments