[isabelle-dev] Crash when using quickcheck

[Christian Weinz]

Hello, 

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. 

A workaround to prevent the crash without completely avoiding quickcheck
would be very welcome. 

Kind regards,
Christian 

---- theory ---- 

theory quickcheck_bug
  imports
    HOL.BNF_Greatest_Fixpoint
    HOL.Quickcheck_Exhaustive
begin

codatatype buggy_type = Buggy_Type (f: int) (s: int)

instantiation buggy_type :: power
begin

primcorec one_buggy_type
  where
    "f 1 = 1"
  | "s 1 = 0"

primcorec times_buggy_type
  where
    "f (x * y) = s y"
  | "s (x * y) = s x * f y"

instance by standard
end

lemma "(Buggy_Type 0 1)^2 = Buggy_Type 1 0"
  quickcheck
  oops

end 

---- error message ---- 

Welcome to Isabelle/HOL (Isabelle2019: June 2019)
message_output terminated
standard_output terminated
standard_error terminated
process terminated
command_input terminated
process_manager terminated
Return code: 139
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20200116/3c0fab0c/attachment.html>