Move prover returns: exiting with verification errors
error: post-condition does not hold
   ┌─ tests/sources/functional/mono.move:71:21
   │
71 │     spec vec_addr { ensures result[0] != @0x1; }
   │                     ^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   =     at tests/sources/functional/mono.move:70: vec_addr
   =         x = <redacted>
   =         x = <redacted>
   =         result = <redacted>
   =     at tests/sources/functional/mono.move:71: vec_addr (spec)

error: post-condition does not hold
   ┌─ tests/sources/functional/mono.move:73:21
   │
73 │     spec vec_bool { ensures result[0] != true; }
   │                     ^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   =     at tests/sources/functional/mono.move:72: vec_bool
   =         x = <redacted>
   =         x = <redacted>
   =         result = <redacted>
   =     at tests/sources/functional/mono.move:73: vec_bool (spec)

error: post-condition does not hold
   ┌─ tests/sources/functional/mono.move:69:20
   │
69 │     spec vec_int { ensures result[0] != 1; }
   │                    ^^^^^^^^^^^^^^^^^^^^^^^
   │
   =     at tests/sources/functional/mono.move:68: vec_int
   =         x = <redacted>
   =         x = <redacted>
   =         result = <redacted>
   =     at tests/sources/functional/mono.move:69: vec_int (spec)

error: post-condition does not hold
   ┌─ tests/sources/functional/mono.move:77:28
   │
77 │     spec vec_struct_addr { ensures result[0].x != @0x1; }
   │                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   =     at tests/sources/functional/mono.move:76: vec_struct_addr
   =         x = <redacted>
   =         x = <redacted>
   =         result = <redacted>
   =     at tests/sources/functional/mono.move:77: vec_struct_addr (spec)

error: post-condition does not hold
   ┌─ tests/sources/functional/mono.move:75:27
   │
75 │     spec vec_struct_int { ensures result[0].x != 1; }
   │                           ^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   =     at tests/sources/functional/mono.move:74: vec_struct_int
   =         x = <redacted>
   =         x = <redacted>
   =         result = <redacted>
   =     at tests/sources/functional/mono.move:75: vec_struct_int (spec)

error: post-condition does not hold
   ┌─ tests/sources/functional/mono.move:82:20
   │
82 │     spec vec_vec { ensures len(result[0]) != 0; }
   │                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   │
   =     at tests/sources/functional/mono.move:79: vec_vec
   =         x = <redacted>
   =     at tests/sources/functional/mono.move:80: vec_vec
   =         x = <redacted>
   =         result = <redacted>
   =     at tests/sources/functional/mono.move:81: vec_vec
   =     at tests/sources/functional/mono.move:82: vec_vec (spec)