Z3 and CVC4 working for Frama-C 22 (Titanium) beta after some initial problems
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.