[isabelle-dev] smt in the repository

[Jasmin Blanchette]

> On 26 May 2020, at 18:08, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> 
> 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.

We have had incidents before when upgrading Z3. Typically what can happen is that Z3 finds a different proof, or uses a different output syntax (or a different corner of its syntax), leading proof reconstruction to fail when it succeeded before. This was quite a big issue, which led Sascha and me to rewrite big parts of the Z3 integration code.

The other thing to keep in mind is that the quantifier instantiation heuristics of SMT solvers are their weak points. Often these thousand-of-clause problems are variable-free or have carefully engineered instantiation triggers. We see on a nearly daily basis that Z3 often isn't strong enough to reconstruct a proof found by CVC4. That's because of the incomplete quantifier instantiation. These are fragile and I wouldn't be surprised if there were regressions from versions to versions.

For years, I haven't been trying to track Z3 development: first, because the parts that interest us are not changing much (they were developed by Leo de Moura), and second, because this would lead to breakages (which I'd have to deal with) and probably little extra happiness overall. So as long as we don't update Z3, we're pretty stable, but we might have problems building old versions for new hardware at some point in the future.

Jasmin