For the final version the code will be kept in a more permanent location.
The why3 file of the case studies: BEMP.mlw.
why3 ide -L . BEMP.mlw
The implementation of the why3 to EVM compiler, cost evaluation the code in the Why3 development branch.
git clone git@gitlab.inria.fr:why3/why3.git
cd why3
git checkout 844e15d
./configure --enable-local
make
bin/why3 extract -D drivers/yul.drv
bench/extraction/extraction_evm.mlw --debug evm_gas_checking > asm.evm
evm --codefile asm.evm --input "14bcc435" run