[isabelle-dev] AFP: Session AVL-Trees broken

[Makarius]

On Tue, 1 Jan 2013, Jasmin Blanchette wrote:

> Am 01.01.2013 um 14:29 schrieb Makarius:
>
>> Testing it briefly myself, it works except for SMT_Word_Examples:
>>
>>  Solver z3: Z3 proof parser (line 2): unknown sort: "bv"
>
> Could you give me some details about how/where this occurs exactly? The "SMT_Word_Examples.thy" file starts with
>
>    declare [[smt_oracle = true]]
>
> As a result, all the certificates in "SMT_Word_Examples.certs" are just one-liner "unsat" proofs -- here's no "line 2" nor any "bv" sort.

I removed all 3 declare commands here: 
http://isabelle.in.tum.de/repos/isabelle/file/fff984a77f58/src/HOL/SMT_Examples/SMT_Word_Examples.thy#l11

Looking more closely again, I now realize that SMT_Examples.thy and 
SMT_Tests.thy have smt_oracle = true, but SMT_Word_Examples.thy smt_oracle 
= true.  So it was a confusion on my side -- but also a potential for user 
confusion.


Anyway, since the "smt" method seems to work right now, I propose to wire 
up a test where smt_certificates and smt_read_only_certificates are left 
unchanged if ISABELLE_FULL_TEST is enabled.  Does that make sense, 
according to the meaning of these options?  SMT/Z3 should run without any 
certificates getting in between.

The conditionioning of the theories can be done with a little bit of ML 
for the options.


 	Makarius