Re: [isabelle] Isabelle2019-RC2 sporadic smt failures



Hi Fabian,


I managed to find an old windows machine and I can reproduce the bug (sometimes at least). And the results are just weird.

smt works as follows:
  (exec 2>&1; z3 ‹input_file›)> ‹temporary_file›

From this, two information are extracted:
  1. the return code to indicate the kind of result (error/unknown)
  2. the temporary_file


Here comes the interesting part. Under heavy load*, the ‹temporary_file› might not contain what I would expect to be there. The content can be corrupted and in particular, it can be empty.



I have no idea what changed since Isabelle2018 that could cause a change in the behaviour. I will think about it, but if anyone has an idea…



Out of curiosity, do you have an SSD or a hard drive?



Best,
Mathias

* I am running Boggie and SMT_Example in parallel in Isabelle/jEdit, based on Pure.


> On 24. May 2019, at 08:43, Mathias Fleury <mathias.fleury12 at gmail.com> wrote:
> 
> 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.