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

[Makarius]

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?


 	Makarius