Move prover returns: exiting with verification errors error: abort not covered by any of the `aborts_if` clauses ┌─ tests/sources/functional/loops.move:86:5 │ 82 │ if (i == 7) abort 7; │ ------- abort happened here with code 0x7 · 86 │ ╭ spec iter10_abort_incorrect { // Disproved. Abort always happens. 87 │ │ pragma verify=true; 88 │ │ aborts_if false; 89 │ │ } │ ╰─────^ │ = at tests/sources/functional/loops.move:77: iter10_abort_incorrect = i = = at tests/sources/functional/loops.move:79: iter10_abort_incorrect = enter loop, variable(s) i havocked and reassigned = i = = loop invariant holds at current state = at tests/sources/functional/loops.move:80: iter10_abort_incorrect = at tests/sources/functional/loops.move:78: iter10_abort_incorrect = at tests/sources/functional/loops.move:82: iter10_abort_incorrect = ABORTED error: unknown assertion failed ┌─ tests/sources/functional/loops.move:235:20 │ 235 │ spec { assert i <= 11; }; // expect to fail, `i` is havoc-ed │ ^^^^^^^^^^^^^^^ │ = at tests/sources/functional/loops.move:233: iter10_assert_instead_of_invariant = i = = at tests/sources/functional/loops.move:235: iter10_assert_instead_of_invariant = enter loop, variable(s) i havocked and reassigned = i = error: function does not abort under this condition ┌─ tests/sources/functional/loops.move:58:9 │ 58 │ aborts_if true; │ ^^^^^^^^^^^^^^^ │ = at tests/sources/functional/loops.move:48: iter10_no_abort_incorrect = i = = at tests/sources/functional/loops.move:50: iter10_no_abort_incorrect = enter loop, variable(s) i havocked and reassigned = i = = loop invariant holds at current state = at tests/sources/functional/loops.move:51: iter10_no_abort_incorrect = at tests/sources/functional/loops.move:49: iter10_no_abort_incorrect = at tests/sources/functional/loops.move:58: iter10_no_abort_incorrect (spec) error: base case of the loop invariant does not hold ┌─ tests/sources/functional/loops.move:210:17 │ 210 │ invariant x != 0; │ ^^^^^^^^^^^^^^^^^ │ = at tests/sources/functional/loops.move:206: loop_invariant_base_invalid = n = = at tests/sources/functional/loops.move:207: loop_invariant_base_invalid = x = = at tests/sources/functional/loops.move:209: loop_invariant_base_invalid = at tests/sources/functional/loops.move:210: loop_invariant_base_invalid error: induction case of the loop invariant does not hold ┌─ tests/sources/functional/loops.move:223:17 │ 223 │ invariant x == 0; │ ^^^^^^^^^^^^^^^^^ │ = at tests/sources/functional/loops.move:219: loop_invariant_induction_invalid = n = = at tests/sources/functional/loops.move:220: loop_invariant_induction_invalid = x = = at tests/sources/functional/loops.move:222: loop_invariant_induction_invalid = at tests/sources/functional/loops.move:223: loop_invariant_induction_invalid = enter loop, variable(s) x havocked and reassigned = x = = loop invariant holds at current state = at tests/sources/functional/loops.move:225: loop_invariant_induction_invalid = at tests/sources/functional/loops.move:221: loop_invariant_induction_invalid = at tests/sources/functional/loops.move:227: loop_invariant_induction_invalid = x = = at tests/sources/functional/loops.move:223: loop_invariant_induction_invalid error: induction case of the loop invariant does not hold ┌─ tests/sources/functional/loops.move:189:17 │ 189 │ invariant x != y; │ ^^^^^^^^^^^^^^^^^ │ = at tests/sources/functional/loops.move:183: loop_with_two_back_edges_incorrect = x = = y = = at tests/sources/functional/loops.move:185: loop_with_two_back_edges_incorrect = at tests/sources/functional/loops.move:188: loop_with_two_back_edges_incorrect = at tests/sources/functional/loops.move:189: loop_with_two_back_edges_incorrect = enter loop, variable(s) x, y havocked and reassigned = x = = y = = loop invariant holds at current state = at tests/sources/functional/loops.move:191: loop_with_two_back_edges_incorrect = at tests/sources/functional/loops.move:192: loop_with_two_back_edges_incorrect = y = = at tests/sources/functional/loops.move:193: loop_with_two_back_edges_incorrect = at tests/sources/functional/loops.move:189: loop_with_two_back_edges_incorrect error: base case of the loop invariant does not hold ┌─ tests/sources/functional/loops.move:145:21 │ 145 │ invariant x != y; │ ^^^^^^^^^^^^^^^^^ │ = at tests/sources/functional/loops.move:138: nested_loop_inner_invariant_incorrect = x = = y = = at tests/sources/functional/loops.move:140: nested_loop_inner_invariant_incorrect = at tests/sources/functional/loops.move:143: nested_loop_inner_invariant_incorrect = enter loop, variable(s) x, y havocked and reassigned = x = = y = = at tests/sources/functional/loops.move:144: nested_loop_inner_invariant_incorrect = at tests/sources/functional/loops.move:145: nested_loop_inner_invariant_incorrect error: induction case of the loop invariant does not hold ┌─ tests/sources/functional/loops.move:145:21 │ 145 │ invariant x != y; │ ^^^^^^^^^^^^^^^^^ │ = at tests/sources/functional/loops.move:138: nested_loop_inner_invariant_incorrect = x = = y = = at tests/sources/functional/loops.move:140: nested_loop_inner_invariant_incorrect = at tests/sources/functional/loops.move:143: nested_loop_inner_invariant_incorrect = enter loop, variable(s) x, y havocked and reassigned = x = = y = = at tests/sources/functional/loops.move:144: nested_loop_inner_invariant_incorrect = at tests/sources/functional/loops.move:145: nested_loop_inner_invariant_incorrect = enter loop, variable(s) y havocked and reassigned = y = = loop invariant holds at current state = at tests/sources/functional/loops.move:147: nested_loop_inner_invariant_incorrect = at tests/sources/functional/loops.move:150: nested_loop_inner_invariant_incorrect = y = = at tests/sources/functional/loops.move:145: nested_loop_inner_invariant_incorrect error: induction case of the loop invariant does not hold ┌─ tests/sources/functional/loops.move:119:17 │ 119 │ invariant x != y; │ ^^^^^^^^^^^^^^^^^ │ = at tests/sources/functional/loops.move:113: nested_loop_outer_invariant_incorrect = x = = y = = at tests/sources/functional/loops.move:115: nested_loop_outer_invariant_incorrect = at tests/sources/functional/loops.move:118: nested_loop_outer_invariant_incorrect = at tests/sources/functional/loops.move:119: nested_loop_outer_invariant_incorrect = enter loop, variable(s) x, y havocked and reassigned = x = = y = = loop invariant holds at current state = at tests/sources/functional/loops.move:122: nested_loop_outer_invariant_incorrect = enter loop, variable(s) y havocked and reassigned = y = = at tests/sources/functional/loops.move:128: nested_loop_outer_invariant_incorrect = at tests/sources/functional/loops.move:131: nested_loop_outer_invariant_incorrect = x = = at tests/sources/functional/loops.move:119: nested_loop_outer_invariant_incorrect