Architecture problem

[Tjark Weber]

On Wed, 2025-10-22 at 09:00 +0200, Jasmin Blanchette wrote:
Tjark Weber's Z3 proof reconstruction code (ITP 2010) might still be alive in HOL4, but I suspect it might not work with a recent Z3.

Ricardo Correia has made numerous improvements to that code and recently updated the supported Z3 version to 4.15.3 (the latest release).

Best,
Tjark








När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20251023/5e1bfcec/attachment.htm>