[isabelle-dev] Status of HOL/SMT

[Makarius]

On Tue, 4 Dec 2012, Jasmin Christian Blanchette wrote:

>> What is also strange is that there seems to be no isatest/mira run that 
>> actually invokes Z3 again on these example theories.
>
> ... nor can there be, with the way in which the certification is 
> hard-coded in them. I don't have a quick solutions for this; problems 
> that Sascha hasn't addressed in four years aren't going to vanish 
> automagically by my putting one lost hour here and there.

If you provide a state where the SMT_Examples session can reproduce its 
proofs, I should be able to wire up some alternative session run with 
[condition=ISABELLE_FULL_TEST].

I've done this recently for several other sessions where that was 
"forgotten", e.g. Sum_of_Squares and the skip_proofs flag.  (For WWW_Find 
I don't know how to do that, so it remains untested and broken for now.)


 	Makarius