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.
- 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.
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.