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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
