<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 Makarius,<div><br></div><div><blockquote type="cite">In particular, the z3 situation is very bad: Could we update that eventually, or discontinue it altogether?<br></blockquote><div>
<meta charset="UTF-8"><div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; 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 dir="auto" style="text-align: start; text-indent: 0px; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div><br></div><div>To summarize a discussion we had together one or two months ago: Z3 has moved on in 11 years, and it would probably be hard to support its new proofs. It's not hard enough for a research project and probably too hard for a BSc and possibly MSc (or at least very supervision-intensive). So we might consider getting rid of Z3 support.</div><div><br></div><div>This means: (1) Sledgehammer should stop generating Z3-based "smt" proofs; (2) we should ask the AFP authors to get rid of their Z3-smt calls (using the more stable veriT or other proofs), maybe with some help from a task force (which I could lead). Do we agree?</div><div><br></div><div>Also unclear in all of this is the role of cvc5. Unlike veriT, it's under active development and is a more complex piece of software (i.e., harder to build). Do we also want to avoid it?</div><div><br></div><div>Best,</div><div>Jasmin</div><div><br></div><div>--</div><div>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 9341<br>Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html<br><br></div></div></div></div></div>
</div>
<div><br><blockquote type="cite"><div>On 21. Oct 2025, at 20:38, Makarius <makarius@sketis.net> wrote:</div><br class="Apple-interchange-newline"><div><div>On 21/10/2025 20:31, Lawrence Paulson wrote:<br><blockquote type="cite">On 21 Oct 2025 at 19:28 +0100, Makarius <makarius@sketis.net>, wrote:<br><blockquote type="cite"><br>That means me need to make more efforts to phase out remaining x86_64-darwin<br>executables, of some external tools. In particular:<br><br>- spass<br>- vampire<br>- verit<br>- smbc<br>- zipperposition<br>- z3<br></blockquote></blockquote><br>> Thanks. I surely hope that we have ARM versions of all of those.<br><br>I also hope it, but this hope is sometimes unfounded.<br><br>In recent years, I have tried hard to support arm64-linux, but a few executables are still missing.<br><br>This year, I have continued under the assumption that x86_64-darwin will stop working soon, but did not yet manage to build all tools yet.<br><br><br>In particular, the z3 situation is very bad: Could we update that eventually, or discontinue it altogether?<br><br><br><span class="Apple-tab-span" style="white-space:pre"> </span>Makarius<br><br></div></div></blockquote></div><br></div></body></html>