ID0002483: **This issue was created automatically from Mantis Issue 2483. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002483 | Frama-C | Plug-in > wp | public | 2019-11-08 | 2019-11-08 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | jens | **Assigned To** | correnson | **Resolution** | open | | **Priority** | normal | **Severity** | minor | **Reproducibility** | always | | **Platform** | Linux | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C GIT, precise the release id | **Target Version** | - | **Fixed in Version** | - | ### Description : I played a bit with various automatic provers in the beta alt-ergo (2.3.0), native:alt-ergo (2.3.0), cvc4 (1.6), cvc3 (2.4.1), z3 (4.8.6) are recognized. Eprover (2.4), on the other hand, is not recognized. To be honest, Eprover is not such a great prover, but it has helped us discovering inconsistencies in our specifications. Is there a specific reason, Eprover is not supported? Attached is the error message. ### Steps To Reproduce : $ frama-c -wp -wp-rte -wp-prover eprover -wp-out abs.wp abs.c [kernel] Parsing abs.c (with preprocessing) [rte] annotating function abs_int [wp] 6 goals scheduled [wp] [Eprover 2.4] Goal typed_abs_int_ensures_3 : Failed [Why3 Error] Unknown printer 'tptp-fof' [wp] [Cache] not used [wp] Proved goals: 5 / 6 Qed: 5 (0.60ms-3ms-6ms) Eprover 2.4: 0 (failed: 1) ## Attachments - [abs.c](/uploads/07380fd95e05b2515b8f7dec3a1bad41/abs.c)