--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on March 2011 ---
Hello Jens and Virgile, I also noticed that Jessie generates VCs for arithmetic safety even if there are no arithmetic operations apart from comparisons. Eg, for enums val1, val2, if(val1 != val2) generates 4 VCs and switch(val1) generates 2 VCs. I don't see how a arithmetic overflow might occur here. What does Jessie try to prover here? Regards, Boris