<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">Hi Larry,<div><br></div><div>"smt(z3" occurs seldom because z3 is the default for "smt", so often it's omitted. (I believe it used to be omitted and now it's explicit.)</div><div><br></div><div>Jasmin</div><div><br><div>
<meta charset="UTF-8"><div dir="auto" style="text-align: start; text-indent: 0px; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div dir="auto" style="text-align: start; text-indent: 0px; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div>--<br>Prof. Dr. Jasmin Blanchette<br>Chair of Theoretical Computer Science and Theorem Proving<br>Ludwig-Maximilians-Universität München<br>Oettingenstr. 67, 80538 München, Germany<br>Tel.: +49 (0)89 2180 9337<br>Email: jasmin.blanchette@ifi.lmu.de<br>Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html<br><br></div></div></div>
</div>
<div><br><blockquote type="cite"><div>On 14. Feb 2024, at 11:42, Lawrence Paulson <lp15@cam.ac.uk> wrote:</div><br class="Apple-interchange-newline"><div><div>Somewhat to my surprise, there seem to be 1004 occurrences of “smt(z3" in the libraries and repository (I've never allowed it personally). It is outnumbered by verit more than 3 to 1, again a surprisingly low ratio. <br><br>Getting rid of them all would be a tedious business. One day we might consider automated tools to crawl over old the proofs and get rid of ugly things. <br><br>Larry<br><br><blockquote type="cite">On 14 Feb 2024, at 07:47, Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de> wrote:<br><br>1. Replace the "smt" calls. Most of them could use the "(verit)" option instead, and for the others, we'd have to come up with alternative proofs. This possibly entails a lot of work, but it could be done by a "task force".<br><br></blockquote><br></div></div></blockquote></div><br></div></body></html>