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

Makarius makarius at sketis.net
Tue Jan 1 22:38:21 CET 2013

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: 

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 

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.


More information about the isabelle-dev mailing list