[isabelle-dev] Status of HOL/SMT
makarius at sketis.net
Tue Dec 4 15:06:44 CET 2012
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
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.)
More information about the isabelle-dev