k-legacy icon indicating copy to clipboard operation
k-legacy copied to clipboard

Published 20 hours ago • verified publisher icon kframework

Smt changes for EVM verification.

Open bmmoore opened this issue 7 years ago • 2 comments

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 avatar Nov 16 '17 22:11 bmmoore

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

bmmoore avatar Nov 17 '17 18:11 bmmoore

@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.

ehildenb avatar Nov 20 '17 20:11 ehildenb