search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

Smt changes for EVM verification. #2373

Open bmmoore opened 6 years ago

bmmoore commented 6 years ago

This adds a missing smtlib attribute necessary for EVM verification, and changes how Z3 presents implications in a way that helps some EVM proofs. For some reason, calling check-sat between asserting the antecedent of an implication and asserting the negation of the consequent allows some things to be proved quickly which would instead timeout (it helps even when the first check-sat call returns "unknown", and other commands that should try to do some solving like (apply smt) do not provide the same benefit).

bmmoore commented 6 years ago

Earlier comments on these changes are at #2369. This rebases and removes some of the changes.

ehildenb commented 6 years ago

@bmmoore I would like to merge this today, but I can't seem to find the relevant branch to rebase on master before merging. There are branches smt and bmmoore/smt, but it appears this PR comes from bmmoore:smt instead (perhaps a different repository)? Either way, can you rebase on master so that we can run the tests on the actual worktree that master will become?

Also, if the other branchs smt and bmmoore/smt are subsumed by this, please delete them.