--- layout: fc_discuss_archives title: Message 85 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Small function with Shifting



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.