hyarion$ frama-c -wp -wp-prover=cvc4,z3-ce isqrt.c
[kernel] Parsing isqrt.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 61 goals scheduled
[wp] Proved goals:   61 / 61
  Qed:            41  (0.30ms-14ms-56ms)
  cvc4:            2  (140ms)
  z3-ce:          19  (30ms-221ms-1.8s)
hyarion$ why3 --version
Why3 platform, version 1.1.0
hyarion$ frama-c -wp -wp-detect
[wp] Prover      Known provers    [Known:provers]
[wp] Prover   Alt-Ergo 2.2.0      [Alt-Ergo:2.2.0]
[wp] Prover       CVC4 1.6        [CVC4:1.6]
[wp] Prover       CVC4 1.6        [CVC4:1.6]
[wp] Prover      Gappa 1.3.2      [Gappa:1.3.2]
[wp] Prover         Z3 4.8.3      [Z3:4.8.3]
[kernel] Warning: no input file.
[wp] 0 goal scheduled
[wp] Proved goals:    0 / 0