Re: [isabelle] Isabelle2019-RC2 sporadic smt failures



On 14/05/2019 13:54, Fabian Immler wrote:
> With Isabelle2019-RC2 on Windows 10, I get sporadic failures of the smt
> method.
> 
> One way to reproduce this is to insert/delete whitespace in the lemma
> statement below. The error 'Solver z3: Solver "z3" failed -- enable
> tracing using the "smt_trace" option for details' will occur in about 1
> out of 10 smt invocations.
> 
> I've attached a trace with [[smt_trace]] enabled.
> 
> 
> theory Scratch
>   imports
>     "HOL-Analysis.Analysis"
> begin
> 
> lemma "fst ((1 - t1) *⇩R fst l1 + t1 *⇩R snd l1) ≤ fst (snd l1)"
>   if "t1 ∈ {0..1}"
>     "p1 = (1 - t1) *⇩R fst l1 + t1 *⇩R snd l1"
>     "fst (fst l1) < fst (snd l1)"
>     "fst (fst l2) < fst (snd l2)"
>     "fst (snd l1) < fst (fst l2)"
>   for l1 l2::"(real*real)*real*real"
>   using that
>   by (smt atLeastAtMost_iff fst_add fst_scaleR scaleR_collapse
> scaleR_left_mono)
> 
> end

This is one of the open obscurities that requires further investigations.

I have copied the above example lemma + proof many times, to get many
tests sequentially (apply ... done) or in parallel (by ...): it works
fine on Linux and 3 different Windows installations.

Do you maybe have some anti-malware software that acts itself as
malware, by hindering external processes?


	Makarius





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