[archi42]

> This checker is proven correct, and because it is simpler, its proof of correctness is easier.

Still correct ;)

What I belief GP (fuklief) meant was: The SMT solver might still be incorrect. Like the register allocator itself in CompCert. But for CompCert, the result is checked by a formally verified checker. I do not know if that's true or not for the result of the SMT solver.

[creata]

Don't SMT solvers output proof objects so that the results can be easily independently verified?

[syrak]

Even if you had a verified SMT checker, you also need to prove that the encoding of the problem in SMT is correct, i.e., that a proof does translate to a valid register allocation solution, to achieve comparable guarantees to CompCert.