Architecture problem

[Jasmin Blanchette]

Thanks for the clarification!

Inspired by this successful porting effort, we could consider updating our code to the latest Z3 as well. I have a bad memory of a previous such port (from 2010 to 2014), but maybe it would go more smoothly this time.

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 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html


> On 23. Oct 2025, at 14:22, Tjark Weber <tjark.weber at it.uu.se> wrote:
> 
> 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/c252029e/attachment.htm>