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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
