Re: [isabelle] Isabelle2019-RC2 sporadic smt failures



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?



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>


I am interested in the statistics at the end, not the proof itself.



Thanks,
Mathias


> 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.