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

[Jasmin Blanchette]

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