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

[Jasmin Blanchette]

Hi Makarius,

> Testing it briefly myself, it works except for SMT_Word_Examples:
> 
>  Solver z3: Z3 proof parser (line 2): unknown sort: "bv"
> 
> Any ideas?

Strange, on my machine everything worked fine (with b1f4291eb916):

    isabelle build HOL-Word-SMT_Examples
    Running HOL-Word-SMT_Examples ...
    Finished HOL-Word-SMT_Examples (0:00:22 elapsed time, 0:00:59 cpu time, factor 2.68)
    0:00:27 elapsed time, 0:01:06 cpu time, factor 2.44

I'll take a closer look.

Jasmin