Smt changes for EVM verification.

[bmmoore]

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]

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

[ehildenb]

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