[Libre-soc-dev] Potential speed up of our mul proofs

Luke Kenneth Casson Leighton lkcl at lkcl.net
Thu Oct 29 21:06:20 GMT 2020

On 10/29/20, Cole Poirier <colepoirier at gmail.com> wrote:
> 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

ah i like the eth-zurich people, very smart.

if it is a plugin into z3 it should be straightforward.

if however it _uses_ z3, not so much.


More information about the Libre-soc-dev mailing list