--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on December 2018 ---
Hi, In order to complete this work around, you can use in addition the option -wp-prop="complete_behaviors_unsatisfiable_requirements" to focus only on detection of inconsistencies in preconditions with eventually a lower time out (-wp-timeout=3 may be enough in practice) . The opposite option -wp-prop="-complete_behaviors_unsatisfiable_requirements" allow you to disable this detection, and focus on the other properties. -- Patrick Baudin > Unfortunately, there is nothing yet into WP for checking > unsatisfiability of function requirements. > > But, there is below a better work around to achive what you done: > - Just add this into your function contract: > >    behavior unsatisfiable_requirements: >         assume \false; >     complete behaviors unsatisfiable_requirements; > > - Then, a successful proof of a such 'complete behaviors' property > means your function requirements are unsatisfiable. > > The benefit of this method is it won't call in question the proof > results of the other properties.