[isabelle-dev] AFP: Session AVL-Trees broken
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