<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style>pre,code,address {
margin: 0px;
}
h1,h2,h3,h4,h5,h6 {
margin-top: 0.2em;
margin-bottom: 0.2em;
}
ol,ul {
margin-top: 0em;
margin-bottom: 0em;
}
blockquote {
margin-top: 0em;
margin-bottom: 0em;
}
</style>
</head>
<body>
<div>On Wed, 2025-10-22 at 09:00 +0200, Jasmin Blanchette wrote:</div>
<blockquote type="cite" style="margin:0 0 0 .8ex; border-left:2px #729fcf solid;padding-left:1ex">
<div>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.</div>
</blockquote>
<div><br>
</div>
<div>Ricardo Correia has made numerous improvements to that code and recently updated the supported Z3 version to 4.15.3 (the latest release).</div>
<div><br>
</div>
<div>Best,</div>
<div>Tjark</div>
<div><span></span></div>
<!DOCTYPE html>
<title>Page Title</title>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
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/
<br>
<br>
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
</body>
</html>