Move prover returns: exiting with verification errors
error: unknown assertion failed
   ┌─ tests/sources/functional/loops_with_memory_ops.move:93:13
   │
93 │             assert forall m in 0..length: a[m] == b[m];
   │             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   =     at tests/sources/functional/loops_with_memory_ops.move:56: nested_loop2
   =     at <internal>:1
   =     at tests/sources/functional/loops_with_memory_ops.move:56: nested_loop2
   =         a = <redacted>
   =         b = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:57: nested_loop2
   =         length = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:59: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:60: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:62: nested_loop2
   =         i = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:63: nested_loop2
   =         x = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:64: nested_loop2
   =         y = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:66: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:67: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:68: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:69: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:70: nested_loop2
   =     enter loop, variable(s) a, b, i, x, y havocked and reassigned
   =         a = <redacted>
   =         b = <redacted>
   =         i = <redacted>
   =         x = <redacted>
   =         y = <redacted>
   =     loop invariant holds at current state
   =     at tests/sources/functional/loops_with_memory_ops.move:67: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:68: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:69: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:70: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:73: nested_loop2
   =     enter loop, variable(s) x, y havocked and reassigned
   =         x = <redacted>
   =         y = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:74: nested_loop2
   =     enter loop, variable(s) y havocked and reassigned
   =         y = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
   =         b = <redacted>
   =         b = <redacted>
   =         a = <redacted>
   =         a = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
   =         i = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:86: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:93: nested_loop2

error: induction case of the loop invariant does not hold
   ┌─ tests/sources/functional/loops_with_memory_ops.move:70:17
   │
70 │                 invariant forall n in 0..i: a[n] == b[n];
   │                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   =     at tests/sources/functional/loops_with_memory_ops.move:56: nested_loop2
   =     at <internal>:1
   =     at tests/sources/functional/loops_with_memory_ops.move:56: nested_loop2
   =         a = <redacted>
   =         b = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:57: nested_loop2
   =         length = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:59: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:60: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:62: nested_loop2
   =         i = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:63: nested_loop2
   =         x = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:64: nested_loop2
   =         y = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:66: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:67: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:68: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:69: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:70: nested_loop2
   =     enter loop, variable(s) a, b, i, x, y havocked and reassigned
   =         a = <redacted>
   =         b = <redacted>
   =         i = <redacted>
   =         x = <redacted>
   =         y = <redacted>
   =     loop invariant holds at current state
   =     at tests/sources/functional/loops_with_memory_ops.move:67: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:68: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:69: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:70: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:73: nested_loop2
   =     enter loop, variable(s) x, y havocked and reassigned
   =         x = <redacted>
   =         y = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:74: nested_loop2
   =     enter loop, variable(s) y havocked and reassigned
   =         y = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:80: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:81: nested_loop2
   =         b = <redacted>
   =         b = <redacted>
   =         a = <redacted>
   =         a = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:85: nested_loop2
   =         i = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:86: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:89: nested_loop2
   =         x = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:90: nested_loop2
   =         y = <redacted>
   =     at tests/sources/functional/loops_with_memory_ops.move:67: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:68: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:69: nested_loop2
   =     at tests/sources/functional/loops_with_memory_ops.move:70: nested_loop2