Frama-C Bug Tracking System - Frama-C
View Issue Details
0002483Frama-CPlug-in > wppublic2019-11-08 12:532019-11-08 12:53
jens 
correnson 
normalminoralways
assignedopen 
Linux
Frama-C GIT, precise the release id 
 
0002483: Eprover in Frama-C 20 beta
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.
$ 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)
No tags attached.
c abs.c (238) 2019-11-08 12:53
https://bts.frama-c.com/file_download.php?file_id=1332&type=bug
Issue History
2019-11-08 12:53jensNew Issue
2019-11-08 12:53jensStatusnew => assigned
2019-11-08 12:53jensAssigned To => correnson
2019-11-08 12:53jensFile Added: abs.c

There are no notes attached to this issue.