--- layout: fc_discuss_archives title: Message 85 from Frama-C-discuss on May 2010 ---
On Thu, 2010-05-20 at 15:30 +0200, Virgile Prevosto wrote: > No, jessie always generates a proof obligation corresponding to the > lemma. However, no automated prover will be able to discharge it > (otherwise, they would prove the PO from the ensures clause directly). > Thus, some additional work is needed (e.g. by using the coq output of > why). I don't understand that why no automatic prover will be able to prove a user-supplied lemma. Isn't this what SMT provers are supposed to do? I thought that a lemma is a way to reduce the search space for the prover by giving it a hint on how to prove the postcondition.