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