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

[Luke Kenneth Casson Leighton]

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.

excellent.

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

l.