move
move copied to clipboard
[Move Prover] Verification timeout when checking two proof targets together
The prover cannot verify two proof targets for the function cmp_bcs_bytes in Compare.move.
The two proof targets can be found here. Both of them involve universal quantifiers with operators on vectors. We suspect this issue may relate to quantifier instantiation. More detailed investigation is needed.