Hi Makarius, 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.
Jasmin -- Prof. Dr. Jasmin Blanchette Chair of Theoretical Computer Science and Theorem Proving Ludwig-Maximilians-Universität München Oettingenstr. 67, 80538 München, Germany Tel.: +49 (0)89 2180 9337 Email: jasmin.blanche...@ifi.lmu.de Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html > On 16. Feb 2024, at 15:33, Makarius <makar...@sketis.net> wrote: > > On 16/02/2024 15:10, Jasmin Blanchette wrote: >> I thought I might make some progress by replacing the "cvc5" binary with >> this script: >> #!/bin/bash >> cp ${!#} "$(mktemp /tmp/foo.XXXXXXXXX).smt" >> /Users/jasminblanchette/.isabelle/contrib/cvc5-1.1.1/arm64-darwin/cvc5.bin $@ >> where "cvc5.bin" is the ARM64 Darwin cvc5 binary. But then the issue doesn't >> arise anymore! > > 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). > > Apart from that, are you satisfied with cvc5-1.1.1? Does everything work with > the current Intel setup? > > If so, I will see how to change our process wrappers such that everything > works again on all platforms. > > > Makarius >
smime.p7s
Description: S/MIME cryptographic signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
