For a solver that is designed to cope with thousands of clauses, I would be surprised if it suffered such a regression that it could fail for the trivial problems we present to it. I’m not aware of an occasion when any of the 2400+ occurrences have ever failed.
I would also question the claim that they are unusually unreadable. The attached list of theorems tends to omit a lot of routine reasoning and therefore lists the critical three or four facts required for the proof. Larry > On 26 May 2020, at 16:58, Tobias Nipkow <[email protected]> wrote: > > Z3 ist not under our control. If it changes, those proofs may no longer work. > Hence I am very sceptical of having them in the distribution. _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
