[isabelle-dev] AFP: Session AVL-Trees broken
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"
More information about the isabelle-dev