<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Hi Larry,<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">I was wanting to know exactly the same thing. In particular, will sledgehammer suggest it now? And does it give us a version of the smt method more robust than the existing one?</div></blockquote><div><br class=""></div></div>That's the goal, but for this to happen, a few small changes (as well as some testing) have to take place. Having the new binaries is the first step. We're (Martin, Mathias, and I) are well aware of the 15 Dec. deadline.<div class=""><br class=""></div><div class="">See also this paper draft for some empirical data:</div><div class=""><br class=""></div><div class=""><span class="Apple-tab-span" style="white-space:pre"> </span><a href="https://matryoshka-project.github.io/pubs/verit_isa_paper.pdf" class="">https://matryoshka-project.github.io/pubs/verit_isa_paper.pdf</a></div><div class=""><br class=""></div><div class="">The nice thing about veriT is that it has more complete instantiation techniques than Z3 -- in fact, more or less the same as implemented in CVC4. This should boost the reconstruction success rate of proofs founds by CVC4.</div><div class=""><br class=""></div><div class="">Jasmin</div><div class=""><br class=""></div></body></html>