*To*: Fabian Immler <immler at in.tum.de>*Subject*: Re: [isabelle] Isabelle2019-RC2 sporadic smt failures*From*: Mathias Fleury <mathias.fleury12 at gmail.com>*Date*: Fri, 24 May 2019 08:43:21 +0200*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <55a9a784-3c25-bbdf-ad3c-74cc57caa5b5@in.tum.de>*References*: <2e8a3e7e-c205-f60f-6b5d-b0353a2618df@sketis.net> <34bd7ccd-778f-effc-a342-158887afee16@in.tum.de> <18c8f524-b61c-1f06-e975-342fe7d11627@sketis.net> <0931F007-447D-471D-B431-28E7AC3DD42F@gmail.com> <55a9a784-3c25-bbdf-ad3c-74cc57caa5b5@in.tum.de>

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 >

**Follow-Ups**:**Re: [isabelle] Isabelle2019-RC2 sporadic smt failures***From:*Mathias Fleury

**References**:**[isabelle] Isabelle2019-RC2 available for testing***From:*Makarius

**[isabelle] Isabelle2019-RC2 sporadic smt failures***From:*Fabian Immler

**Re: [isabelle] Isabelle2019-RC2 sporadic smt failures***From:*Makarius

**Re: [isabelle] Isabelle2019-RC2 sporadic smt failures***From:*Mathias Fleury

**Re: [isabelle] Isabelle2019-RC2 sporadic smt failures***From:*Fabian Immler

- Previous by Date: Re: [isabelle] Isabelle2019-RC2 sporadic smt failures
- Next by Date: Re: [isabelle] Algebraic rule collections
- Previous by Thread: Re: [isabelle] Isabelle2019-RC2 sporadic smt failures
- Next by Thread: Re: [isabelle] Isabelle2019-RC2 sporadic smt failures
- Cl-isabelle-users May 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list