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

[Jasmin Blanchette]

Reviving an old thread:

Am 12.12.2012 um 11:47 schrieb Makarius:

> On Wed, 12 Dec 2012, Jasmin Christian Blanchette wrote:
> 
>> Right now I am experiencing lots of failures -- typically Z3 3.2 returning with error code 112. I don't know if it's an instance of the same bug, but as long as this is broken it's hard to know.
> 
> I've seen spurious error 112 myself when I tried Z3 3.2 vs. 4.0 recently. I could not pin it down exactly, so I merely left it on my private TODO list to see again later.  There might be a slight tendency of such failures on Mac OS X, but this is just speculation.

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. I'll push the fix later today once I've regenerated the certificates.

Gutes neues Jahr!

Jasmin