3 ms·

Let's say that through Why3 they manage to harness all kinds of SMT solvers (and others like grappa?).