Prover changes for EVM ABI verification

kframework / k-legacy

The K tools (deprecated, see README)

http://kframework.org

Other

146 stars 61 forks source link

Closed bmmoore closed 6 years ago

bmmoore commented 6 years ago

Adds smtlib attributes to a few builtins, and changes the generated Z3 querys to something which is much faster in some proofs.

kframework-bot commented 6 years ago

Can one of the admins verify this patch?

msaxena2 commented 6 years ago

test this please

bmmoore commented 6 years ago

The string builtin seems to be problematic for some tests, so I'm making a smaller version of this pull request.