[isabelle-dev] smt in the repository

Lawrence Paulson lp15 at cam.ac.uk
Tue May 26 18:08:57 CEST 2020

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.


> On 26 May 2020, at 16:58, Tobias Nipkow <nipkow at in.tum.de> 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.

More information about the isabelle-dev mailing list