Found this SMT solver 'thing' which is built on top of z3, which is what I think we are currently using... unless we're using symiyosys or yices. Perhaps this could speed up our mul proofs by an order of magnitude? Thoughts? I've linked it on the wiki resources page. https://github.com/eth-sri/fastsmt Cole