Is it to possible to export or log the SAT/SMT-equations that are generated by FRAMA-C/WP and Why3 sent for discharge to a SAT-SMT-Solver like Alt-Ergo or Z3?
In case the solver Z3 is used (e.g. via the command frama-c -wp -wp-prover z3 test.c) would it also be possible to export the generated SMT-equations in smt-lib-format?
I am wondering whether these exported equations could further be used to obtain counter-examples?
I tried using the -wp-out dir-flag which did not generate any output. My version of frama-c is: 26.1 (Iron) and why3: 1.5.1
Exporting SMT solver files is currently not implemented. It is not hard to add but requires adding a new option to Frama-C for this. Exploiting these files to get counter example is probably possible but that would not be that direct because without the right description of the proof context, it might give counter examples that are not that interesting.
Basically, to be useful the counter example must expose values that correspond to function inputs. Thus, this need to be explained to SMT solvers so that they instantiate the right variables. Because of simplifications produced by Qed before sending the PO to Why3, the different names of variables might not be that easy to infer, it would be more efficient if WP could do it for us.
There is existing work for the implementation of counter examples in WP, but it is not ready to be released and requires more development effort.