<html><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /></head><body style='font-size: 10pt; font-family: Verdana,Geneva,sans-serif'>
<p>Hello,</p>
<p>I stumbled across a crash in Isabelle2019. I did my best to create a reasonably small theory that results in a crash. The theory given below crashes upon reaching the quickcheck. The resulting error message is given below, too. If more information is necessary, I'd be glad to provide it.</p>
<p>A workaround to prevent the crash without completely avoiding quickcheck would be very welcome.</p>
<p>Kind regards,<br />Christian</p>
<p>---- theory ----</p>
<p>theory quickcheck_bug<br /> imports<br /> HOL.BNF_Greatest_Fixpoint<br /> HOL.Quickcheck_Exhaustive<br />begin<br /><br />codatatype buggy_type = Buggy_Type (f: int) (s: int)<br /><br />instantiation buggy_type :: power<br />begin<br /><br />primcorec one_buggy_type<br /> where<br /> "f 1 = 1"<br /> | "s 1 = 0"<br /><br />primcorec times_buggy_type<br /> where<br /> "f (x * y) = s y"<br /> | "s (x * y) = s x * f y"<br /><br />instance by standard<br />end<br /><br />lemma "(Buggy_Type 0 1)^2 = Buggy_Type 1 0"<br /> quickcheck<br /> oops<br /><br />end</p>
<p>---- error message ----</p>
<p>Welcome to Isabelle/HOL (Isabelle2019: June 2019)<br />message_output terminated<br />standard_output terminated<br />standard_error terminated<br />process terminated<br />command_input terminated<br />process_manager terminated<br />Return code: 139</p>
<div> </div>
</body></html>