[isabelle-dev] smt in the repository

[Lawrence Paulson]

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 <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.