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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
