Re: [isabelle] Isabelle2019-RC2 sporadic smt failures



On 27/05/2019 12:14, Fabian Immler wrote:
> On 5/27/2019 11:26 AM, Makarius wrote:
>> On 26/05/2019 08:56, Fabian Immler wrote:
>>>>
>>>> The above changes are already in Isabelle2019-RC3. Can you try if it
>>>> makes a difference.
>>> It is better now, but I still get 6-7 failures in 400 runs. (It was 20
>>> failures with Isabelle2019-RC2)
>>
>> Is there an easy way to provide the 400 runs above as isolated example?
> Not sure if that is what you mean, but I was referring to simply 400
> copies of the smt-call that I reported earlier in this thread:

OK, I will try this. I've thought that you have an actual application
with 400 runs somewhere in the background.

The implicit question behind this: How serious is the impact on
applications?

I will make one more round of refinement, but it might be all we can do
for now (the Isabelle2019 release).


	Makarius




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