Architecture problem

[Lawrence Paulson]

They appeared to be nearly 1300 occurrences of “smt (z3" in over 300 different files. Ideally the change would be automated. One would like to think that one of the other solvers would be good enough to serve as a drop-in replacement for 15 year-old code, but maybe not.

Larry

> On 21 Oct 2025, at 19:44, Jasmin Blanchette <jasmin.blanchette at ifi.lmu.de> wrote:
> 
> So we might consider getting rid of Z3 support.
> 
> This means: (1) Sledgehammer should stop generating Z3-based "smt" proofs; (2) we should ask the AFP authors to get rid of their Z3-smt calls (using the more stable veriT or other proofs), maybe with some help from a task force (which I could lead). Do we agree?