move icon indicating copy to clipboard operation
move copied to clipboard

[Move Prover] Verification timeout when checking two proof targets together

Open rahxephon89 opened this issue 3 years ago • 0 comments

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.

rahxephon89 avatar Nov 16 '21 18:11 rahxephon89