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

_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to