Architecture problem

Lawrence Paulson lp15 at cam.ac.uk
Tue Oct 21 20:47:23 CEST 2025


Did you see the ITP paper "Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL”? It was for cvc5.

Larry
On 21 Oct 2025 at 19:38 +0100, Jasmin Blanchette <jasmin.blanchette at ifi.lmu.de>, wrote:

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?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20251021/05f0a69a/attachment.htm>


More information about the isabelle-dev mailing list