Re: [isabelle] Isabelle2019-RC2: Prover errors when using sledgehammer



On 27/05/2019 11:15, Makarius wrote:
> 
> I somehow suspect that the problems we see now are due to the change of
> the environment, i.e. latent fragilities now become apparent due to one
> or more of these reasons:
> 
>   * unknown changes in Cygwin (64bit version, other changes)
>   * unknown changes in Windows 10
>   * unknown changes in the hardware: much faster process creation due to
> SSD etc.
> 
> (I will continue on a different side-branch of this thread.)

Actually, we have two different threads, and the problems might be
unrelated:

  (1) "Prover errors when using sledgehammer" (Pater Lammich): timeout
of Z3 sometimes shows up as "prover error" (presumably on all platforms)

  (2) "sporadic smt failures" (Fabian Immler): z3 behind the "smt" proof
method sometimes fails spontaneously (on Windows).


	Makarius





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