GitLab

I updated the title after figuring out a solution

• the issue has not yet been reported on Gitlab;
• the issue has not yet been reported on our BTS;
• you installed Frama-C as prescribed in the instructions.

Contextual information

• Frama-C installation mode: Opam
• Frama-C version: 22.0-beta (Titanium)
• Plug-in used: WP
• OS name: Xubuntu
• OS version: Ubuntu 20.04.1 LTS

Please add specific information deemed relevant with regard to this issue.

I am able to use the options -wp-prover Alt-Ergo -wp-prover native:coq with ACSL by Example. However when using either -wp-prover Z3 or -wp-prover z3 I receive the following error message. (Note that z3 (4.8.6) has been installed and that it has been successfully registered with why3 config --full-config)

[kernel] Parsing find.c (with preprocessing)
[rte] annotating function find
[wp] User Error: Prover 'z3' not found in why3.conf
[wp] Warning: native support for coq is deprecated, use tip instead
[wp] 25 goals scheduled
[wp] Proved goals:   25 / 25
  Qed:              16  (2ms-6ms-20ms)
  Alt-Ergo 2.3.3:    9  (5ms-12ms) (87)
[wp] User Error: Deferred error message was emitted during execution. See above messages for more information.
[kernel] Plug-in wp aborted: invalid user input.

Similar with CVC4 and cvc4.