Move prover returns: exiting with verification errors error: post-condition does not hold ┌─ tests/sources/functional/choice.move:301:9 │ 301 │ ╭ ensures !(get_ballot(signer::address_of(ballot_account), result).expiration_timestamp_secs 302 │ │ <= 0); │ ╰──────────────────^ │ = at tests/sources/functional/choice.move:279: create_ballot = ballot_account = = at tests/sources/functional/choice.move:283: create_ballot = at tests/sources/functional/choice.move:282: create_ballot = at tests/sources/functional/choice.move:290 = at tests/sources/functional/choice.move:285: create_ballot = at tests/sources/functional/choice.move:271: new_ballot_id = counter = = at tests/sources/functional/choice.move:274: new_ballot_id = result = = at tests/sources/functional/choice.move:277: new_ballot_id = ballot_id = = at tests/sources/functional/choice.move:286: create_ballot = result = = at tests/sources/functional/choice.move:287: create_ballot = at tests/sources/functional/choice.move:301: create_ballot (spec) error: post-condition does not hold ┌─ tests/sources/functional/choice.move:55:9 │ 55 │ ensures choice == signer::address_of(s2); │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ │ = at tests/sources/functional/choice.move:45: populate_R = at tests/sources/functional/choice.move:50: populate_R (spec) = at tests/sources/functional/choice.move:51: populate_R (spec) = at tests/sources/functional/choice.move:54: populate_R (spec) = at tests/sources/functional/choice.move:53: populate_R (spec) = at tests/sources/functional/choice.move:45: populate_R = s1 = = s2 = = at tests/sources/functional/choice.move:46: populate_R = at tests/sources/functional/choice.move:47: populate_R = at tests/sources/functional/choice.move:48: populate_R = at tests/sources/functional/choice.move:55: populate_R (spec) error: post-condition does not hold ┌─ tests/sources/functional/choice.move:22:9 │ 22 │ ensures result == TRACE(choose x: u64 where x >= 4 && x <= 5); │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ │ = at tests/sources/functional/choice.move:16: simple_incorrect = b = = at tests/sources/functional/choice.move:17: simple_incorrect = result = = at tests/sources/functional/choice.move:18: simple_incorrect = at tests/sources/functional/choice.move:22: simple_incorrect (spec) = `TRACE(choose x: u64 where x >= 4 && x <= 5)` = error: post-condition does not hold ┌─ tests/sources/functional/choice.move:99:9 │ 99 │ ensures result == TRACE(choose y: u64 where y > x); │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ │ = at tests/sources/functional/choice.move:94: test_choice_dup_expected_fail = x = = at tests/sources/functional/choice.move:95: test_choice_dup_expected_fail = result = = at tests/sources/functional/choice.move:96: test_choice_dup_expected_fail = at tests/sources/functional/choice.move:99: test_choice_dup_expected_fail (spec) = `TRACE(choose y: u64 where y > x)` = error: post-condition does not hold ┌─ tests/sources/functional/choice.move:157:9 │ 157 │ ensures evidence1 == evidence2; │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ │ = at tests/sources/functional/choice.move:155: test_different_choice_via_let (spec) = at tests/sources/functional/choice.move:156: test_different_choice_via_let (spec) = at tests/sources/functional/choice.move:153: test_different_choice_via_let = at tests/sources/functional/choice.move:157: test_different_choice_via_let (spec) error: post-condition does not hold ┌─ tests/sources/functional/choice.move:181:9 │ 181 │ ensures choose_some_positive_u64() == choose_another_positive_u64(); │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ │ = at tests/sources/functional/choice.move:179: test_different_choice_via_spec_fun = at tests/sources/functional/choice.move:181: test_different_choice_via_spec_fun (spec) error: post-condition does not hold ┌─ tests/sources/functional/choice.move:71:9 │ 71 │ ensures (choose min i in 0..len(result) where result[i] == 2) == 1; │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ │ = at tests/sources/functional/choice.move:62: test_min = v = = at tests/sources/functional/choice.move:63: test_min = v_ref = = at tests/sources/functional/choice.move:64: test_min = at tests/sources/functional/choice.move:65: test_min = at tests/sources/functional/choice.move:66: test_min = at tests/sources/functional/choice.move:67: test_min = v = = at tests/sources/functional/choice.move:68: test_min = result = = at tests/sources/functional/choice.move:69: test_min = at tests/sources/functional/choice.move:71: test_min (spec) error: post-condition does not hold ┌─ tests/sources/functional/choice.move:86:9 │ 86 │ ensures TRACE(choose i in 0..len(result) where result[i] == 2) == 1; │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ │ = at tests/sources/functional/choice.move:75: test_not_using_min_incorrect = v = = at tests/sources/functional/choice.move:76: test_not_using_min_incorrect = v_ref = = at tests/sources/functional/choice.move:77: test_not_using_min_incorrect = at tests/sources/functional/choice.move:78: test_not_using_min_incorrect = at tests/sources/functional/choice.move:79: test_not_using_min_incorrect = at tests/sources/functional/choice.move:80: test_not_using_min_incorrect = at tests/sources/functional/choice.move:81: test_not_using_min_incorrect = v = = at tests/sources/functional/choice.move:82: test_not_using_min_incorrect = result = = at tests/sources/functional/choice.move:83: test_not_using_min_incorrect = at tests/sources/functional/choice.move:86: test_not_using_min_incorrect (spec) = `TRACE(choose i in 0..len(result) where result[i] == 2)` = error: post-condition does not hold ┌─ tests/sources/functional/choice.move:218:9 │ 218 │ ensures result != (choose i: u64 where i >= k); │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ │ = at tests/sources/functional/choice.move:235: test_same_choice_different_args_via_schema_2 = result = = at tests/sources/functional/choice.move:236: test_same_choice_different_args_via_schema_2 = at tests/sources/functional/choice.move:218 error: post-condition does not hold ┌─ tests/sources/functional/choice.move:209:9 │ 209 │ ensures evidence1 == evidence2; │ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ │ = at tests/sources/functional/choice.move:205: test_same_choice_different_args_via_spec_fun = at tests/sources/functional/choice.move:207: test_same_choice_different_args_via_spec_fun (spec) = at tests/sources/functional/choice.move:208: test_same_choice_different_args_via_spec_fun (spec) = at tests/sources/functional/choice.move:205: test_same_choice_different_args_via_spec_fun = x = = y = = result = = at tests/sources/functional/choice.move:209: test_same_choice_different_args_via_spec_fun (spec)