Re: [isabelle] Isabelle2019-RC2 sporadic smt failures



Thank you very much for the detailed information.


To give you idea, on my mac I get

:total-time           0.01


So z3 on my machine is around ten times faster (!) on that problem.


I will try to play with the timeout to see if I can reproduce the problem.


Mathias


> On 24. May 2019, at 07:48, Fabian Immler <immler at in.tum.de> wrote:
> 
> 
> 
> On 5/23/2019 5:54 PM, Mathias Fleury wrote:
>> Hi Fabian,
>> Can you replace in ~~/src/Tools/SMT/smt_systems.ML:
>> fun outcome_of unsat sat unknown solver_name line =
>>   if String.isPrefix unsat line then SMT_Solver.Unsat
>>   else if String.isPrefix sat line then SMT_Solver.Sat
>>   else if String.isPrefix unknown line then SMT_Solver.Unknown
>>   else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^ quote solver_name ^
>>     " failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^
>>     " option for details"))
>> by
>> fun outcome_of unsat sat unknown solver_name line =
>>   if String.isPrefix unsat line then SMT_Solver.Unsat
>>   else if String.isPrefix sat line then SMT_Solver.Sat
>>   else if String.isPrefix unknown line then SMT_Solver.Unknown
>>   else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^ quote solver_name ^
>>     " failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^
>>     " option for details and the error is " ^ (@{make_string} line)))
>> and then run your example (you will have to recompile HOL and HOL-Analysis) and after that tell me the exact error message?
> Yes, I replaced it (in ~~/src/HOL/Tools/SMT/smt_systems.ML) and got:
> Solver z3: Solver "z3" failed -- enable tracing using the "smt_trace" option for details and the error is ""
> 
>> Moreover could you run put the SMT problem outside of Isabelle in a terminal (I have attached the file, but it is exactly the problem that is included in your message) with the following command:
>> $ ~/.isabelle/contrib/z3-4.4.0pre-2/x86-windows/z3 --st smt.random_seed=1 smt.refine_inj_axioms=false -T:20 <path/to/prob_z3.smt_in>
> Yes, I ran this from ~/.isabelle/contrib and also from .../Isabelle2019-RC2/contrib.
> It works fine all the time (for 100+ sequential runs)
> 
>> I am interested in the statistics at the end, not the proof itself.
> (:add-rows             23
> :added-eqs            29
> :arith-conflicts      1
> :assert-lower         15
> :assert-upper         19
> :conflicts            1
> :eq-adapter           15
> :fixed-eqs            6
> :max-generation       3
> :memory               0.61
> :mk-clause            43
> :num-checks           1
> :pivots               12
> :propagations         17
> :quant-instantiations 27
> :time                 0.00
> :total-time           1.16)



> 
> Fabian
> 
>>> On 23. May 2019, at 17:19, Makarius <makarius at sketis.net> wrote:
>>> 
>>> 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.