--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on April 2020 ---
Hello, The option -wp-prop allows to prove properties (annotations) with a particular name, say â-wp-prop=unchangedâ . However, I often have several post conditions, loop invariant and assertion with the name âunchangedâ and I am not always interested to verify all of them but only a specific generated proof obligations. My question is if there is an option to verify a particular proof obligation by supplying its âinternalâ names such as typed_external_push_heap_ensures_unchanged ? Regards Jens