Re: [isabelle] Isabelle2019-RC2 sporadic smt failures





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


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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