--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on June 2011 ---
> In that case, frama-c/ Jessie will check the postcondition for the cases > that (x=1 and x=3) as well as (x=1 and x=4) and go on.. > > Unless that normally we will never have both x= 1 and x= 3 at the same time. Oh, I think I understand your question now. You are looking at the various goals generated for the single post-condition and you see things such as: integer_of_int32(x_0) = 3 and: integer_of_int32(x_0) = 5 as hypotheses for the same goal, and you are wondering why Why considers this impossible case. This is normal. It has not started to think yet at the time it has generated these two incompatible hypotheses. Don't worry, automated theorem provers are very good at noticing that there is \false in the hypotheses and concluding directly (here, reproducing the reasoning that whatever logical property needs to be verified is true because the case where x is both 3 and 5 simultaneously never happens). If you are worried that with all these impossible cases, the total number of goals will be too large, use option -jessie-why-opt="-fast-wp". This will generate a single goal, which will of course be more complex. Pascal