--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on December 2014 ---
Le 15/12/2014 10:04, Lo?c Correnson a ?crit : > Indeed, for simple PO discharged by Qed, there is actually no other proof obligation but ? goal PO : true ? ! > You can try to deactivate the advanced simplifications of WP with `-wp-no-let` and other options of the same group, but most very low-level simplifications such as ? 1+2 ? into ? 3 ? or ? a+0 = a ? are always applied and can not be deactivated. OK, thanks. Best regards, david