[isabelle] sledgehammer (or Z3) internal error

The attached theory causes a sledgehammer error in Isabelle 2020.

The theory is as small as I have been able to make it. Seemingly unrelated things like the datatype declaration, the function p and even the locale names (!) matter.

Even more odd is that editing the theory in Isabelle and then undoing the edits sometimes causes the error to go away. Loading the theory in a fresh instance of Isabelle always triggers the error, however.


Lars-Henrik Eriksson, PhD, Senior Lecturer
Computing Science, Dept. of Information Technology, Uppsala University, Sweden
E-mail: lhe at it.uu.se, Web: http://www.it.uu.se/katalog/lhe?lang=en
Phone: +46 18 471 10 57, Mobile: +46 705-36 39 16, Fax: +46 18 51 19 25

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

Attachment: Z3bug.thy
Description: Binary data

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.