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

Makarius makarius at sketis.net
Tue Jan 1 14:29:56 CET 2013

On Tue, 1 Jan 2013, Jasmin Blanchette wrote:

> I found out what this error code 112 is, the cause, and its fix. 112 
> means that the user-specified soft timeout has been reached. The soft 
> timeout argument was introduced by my change 34b0464d7eef; Z3 expects 
> milliseconds and I passed seconds.

Great, one step further towards the release.

Testing it briefly myself, it works except for SMT_Word_Examples:

   Solver z3: Z3 proof parser (line 2): unknown sort: "bv"

Any ideas?


More information about the isabelle-dev mailing list