Junkil Park

Work in progress - Prover has some unknown performance issue with the new version of Z3 and Boogie. ## Motivation To bump up the version number of Prover's deps. ###...

the issue with "transaction ran out of gas" appears again. this time, array arguments in external calls are suspicious. See the following in `ExternalCall.test.js`: ``` // TODO: Error with "Transaction...

See `ExternalCall.move`. As the "TODO" says, it's expected to revert with the reason string which come from the callee. However, it reverts without any string. ``` // TODO: The following...

value comparison (`vec_u8_1 == vec_u8_2`) works but not reference comparison. However, this is not a blocker for the demo.

- Gave a better link rather than the link to the example folder.

# 🐛 Bug Prover (`move-model`) panics if `T` does not have the "struct" type in the spec expression `exists(0x1)`. ## To reproduce **Code snippet to reproduce** ``` struct R has...

# 🐛 Bug Boogie (sometimes) exited with an error due to an unhandled exception. ## To reproduce It's hard to reproduce. However, the following script can help reproducing it. **Code...

In the daily test, `MVP_TEST_ON_CI` is on. When it's on, even though `MVP_TEST_FEATURE=cvc4` is given, the cvc4 tests are ignored. So, with `MVP_TEST_ON_CI=1` and `MVP_TEST_FEATURE=cvc4`, it basically tests nothing. The...

# 🚀 Feature Request A .move file can only contain some specs for Move Prover. For example, see the following link: https://github.com/move-language/move/blob/main/language/extensions/move-table-extension/sources/Table.spec.move Currently, `move-analyzer` does not handle these spec files...