--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on November 2019 ---
Hello Virgile, thank you very much for the hint with 'native:coq". By calling 'frama-c -wp-help' I have found out that '-wp-script' is now probably '-wp-coq-script'. This is certainly a better name but this change should be better documented. If why3 is now used at compile time, is it then still necessary to call "why3 config --detect" after the installation of provers? I also received a couple of warning for various provers along the lines of Eprover 2.4: Failed [Why3 Error] anomaly: Why3.Whyconf.StepsCommandNotSpecified("The solver is used with a step limit and the command for running the solver with a step limit is not specified.") Coq 8.9.1: Failed [Why3 Error] anomaly: Why3.Whyconf.StepsCommandNotSpecified("The solver is used with a step limit and the command for running the solver with a step limit is not specified.") Regards Jens