<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>I'm very satisfied with cvc5. I ran an evaluation on hundreds of goals from the AFP and the success rate went up from 52% for CVC4 to 64% for cvc5.</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 16. Feb 2024, at 15:33, Makarius <makarius@sketis.net> wrote:</div><br class="Apple-interchange-newline"><div><div>On 16/02/2024 15:10, Jasmin Blanchette wrote:<br><blockquote type="cite">I thought I might make some progress by replacing the "cvc5" binary with this script:<br>#!/bin/bash<br>cp ${!#} "$(mktemp /tmp/foo.XXXXXXXXX).smt"<br>/Users/jasminblanchette/.isabelle/contrib/cvc5-1.1.1/arm64-darwin/cvc5.bin $@<br>where "cvc5.bin" is the ARM64 Darwin cvc5 binary. But then the issue doesn't arise anymore!<br></blockquote><br>That could be some odd effect from switching between Intel and ARM on macOS, maybe caused by our bash_process wrapper (which is for Intel in Isabelle/0f01c575ff3e).<br><br>Apart from that, are you satisfied with cvc5-1.1.1? Does everything work with the current Intel setup?<br><br>If so, I will see how to change our process wrappers such that everything works again on all platforms.<br><br><br><span class="Apple-tab-span" style="white-space:pre"> </span>Makarius<br><br></div></div></blockquote></div><br></div></body></html>