Move prover returns: exiting with verification errors
error: post-condition does not hold
   ┌─ tests/sources/functional/macro_verification.move:32:9
   │
32 │         ensures forall i in range(v): v[i] == old(v)[i] + 2; // fails
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   = Related Bindings:
   =         old(v) = <redacted>
   =         v = <redacted>
   = Execution Trace:
   =     at tests/sources/functional/macro_verification.move:15: foreach
   =     at <internal>:1
   =     at tests/sources/functional/macro_verification.move:15: foreach
   =         v = <redacted>
   =     at tests/sources/functional/macro_verification.move:16: foreach
   =         i = <redacted>
   =     at tests/sources/functional/macro_verification.move:22: foreach
   =     at tests/sources/functional/macro_verification.move:23: foreach
   =         `invariant i >= 0 && i <= len(v);` = <redacted>
   =     at tests/sources/functional/macro_verification.move:24: foreach
   =         `invariant len(v) == len(old(v));` = <redacted>
   =     at tests/sources/functional/macro_verification.move:25: foreach
   =         `invariant forall j in 0..i: v[j] == old(v)[j] + 1;` = <redacted>
   =     at tests/sources/functional/macro_verification.move:26: foreach
   =         `invariant forall j in i..len(v): v[j] == old(v)[j];` = <redacted>
   =     enter loop, variable(s) v, i havocked and reassigned
   =         v = <redacted>
   =         i = <redacted>
   =         `invariant forall j in i..len(v): v[j] == old(v)[j];` = <redacted>
   =     loop invariant holds at current state
   =     at tests/sources/functional/macro_verification.move:23: foreach
   =         `invariant i >= 0 && i <= len(v);` = <redacted>
   =     at tests/sources/functional/macro_verification.move:24: foreach
   =         `invariant len(v) == len(old(v));` = <redacted>
   =     at tests/sources/functional/macro_verification.move:25: foreach
   =         `invariant forall j in 0..i: v[j] == old(v)[j] + 1;` = <redacted>
   =     at tests/sources/functional/macro_verification.move:26: foreach
   =         `invariant forall j in i..len(v): v[j] == old(v)[j];` = <redacted>
   =     at tests/sources/functional/macro_verification.move:17: foreach
   =     at tests/sources/functional/macro_verification.move:27: foreach
   =         v = <redacted>
   =     at tests/sources/functional/macro_verification.move:30: foreach (spec)
   =         `ensures len(v) == len(old(v));` = <redacted>
   =     at tests/sources/functional/macro_verification.move:31: foreach (spec)
   =         `ensures forall i in range(v): v[i] == old(v)[i] + 1;` = <redacted>
   =     at tests/sources/functional/macro_verification.move:32: foreach (spec)
   =         `ensures forall i in range(v): v[i] == old(v)[i] + 2;` = <redacted>

error: post-condition does not hold
   ┌─ tests/sources/functional/macro_verification.move:57:9
   │
57 │         ensures len(v) <= 4 ==> result == spec_sum(v, len(v)) + 1; // fails
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   = Related Bindings:
   =         result = <redacted>
   =         spec_sum(v, len(v)) = <redacted>
   =         v = <redacted>
   = Execution Trace:
   =     at tests/sources/functional/macro_verification.move:40: reduce
   =         v = <redacted>
   =     at tests/sources/functional/macro_verification.move:41: reduce
   =         i = <redacted>
   =     at tests/sources/functional/macro_verification.move:42: reduce
   =         sum = <redacted>
   =     at tests/sources/functional/macro_verification.move:48: reduce
   =     at tests/sources/functional/macro_verification.move:49: reduce
   =         `invariant i >= 0 && i <= len(v);` = <redacted>
   =     at tests/sources/functional/macro_verification.move:50: reduce
   =         `invariant sum == spec_sum(v, i);` = <redacted>
   =     enter loop, variable(s) i, sum havocked and reassigned
   =         i = <redacted>
   =         sum = <redacted>
   =         `invariant sum == spec_sum(v, i);` = <redacted>
   =     loop invariant holds at current state
   =     at tests/sources/functional/macro_verification.move:49: reduce
   =         `invariant i >= 0 && i <= len(v);` = <redacted>
   =     at tests/sources/functional/macro_verification.move:50: reduce
   =         `invariant sum == spec_sum(v, i);` = <redacted>
   =     at tests/sources/functional/macro_verification.move:43: reduce
   =     at tests/sources/functional/macro_verification.move:52: reduce
   =         result = <redacted>
   =     at tests/sources/functional/macro_verification.move:55: reduce (spec)
   =         `ensures result == spec_sum(v, len(v));` = <redacted>
   =     at tests/sources/functional/macro_verification.move:57: reduce (spec)
   =         `ensures len(v) <= 4 ==> result == spec_sum(v, len(v)) + 1;` =
   =           <redacted>

error: post-condition does not hold
   ┌─ tests/sources/functional/macro_verification.move:76:9
   │
76 │         ensures result == x + y + y; // fails
   │         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   = Related Bindings:
   =         result = <redacted>
   =         x = <redacted>
   =         y = <redacted>
   = Execution Trace:
   =     at tests/sources/functional/macro_verification.move:67: reduce_test
   =         x = <redacted>
   =         y = <redacted>
   =         z = <redacted>
   =     at tests/sources/functional/macro_verification.move:68: reduce_test
   =         v = <redacted>
   =     at tests/sources/functional/macro_verification.move:69: reduce_test
   =         v = <redacted>
   =     at tests/sources/functional/macro_verification.move:70: reduce_test
   =         v = <redacted>
   =     at tests/sources/functional/macro_verification.move:71: reduce_test
   =         v = <redacted>
   =     at tests/sources/functional/macro_verification.move:72: reduce_test
   =     at tests/sources/functional/macro_verification.move:40: reduce
   =         v = <redacted>
   =     at tests/sources/functional/macro_verification.move:41: reduce
   =         i = <redacted>
   =     at tests/sources/functional/macro_verification.move:42: reduce
   =         sum = <redacted>
   =     at tests/sources/functional/macro_verification.move:48: reduce
   =     at tests/sources/functional/macro_verification.move:49: reduce
   =     at tests/sources/functional/macro_verification.move:50: reduce
   =     enter loop, variable(s) i, sum havocked and reassigned
   =         i = <redacted>
   =         sum = <redacted>
   =     loop invariant holds at current state
   =     at tests/sources/functional/macro_verification.move:49: reduce
   =     at tests/sources/functional/macro_verification.move:50: reduce
   =     at tests/sources/functional/macro_verification.move:43: reduce
   =     at tests/sources/functional/macro_verification.move:52: reduce
   =         result = <redacted>
   =     at tests/sources/functional/macro_verification.move:53: reduce
   =         result = <redacted>
   =     at tests/sources/functional/macro_verification.move:73: reduce_test
   =     at tests/sources/functional/macro_verification.move:75: reduce_test (spec)
   =         `ensures result == x + y + z;` = <redacted>
   =     at tests/sources/functional/macro_verification.move:76: reduce_test (spec)
   =         `ensures result == x + y + y;` = <redacted>