--- layout: fc_discuss_archives title: Message 54 from Frama-C-discuss on November 2013 ---
On 08/11/2013 04:25, John Regehr wrote: > The functions below have identical specifications and are functionally > equivalent. All provers (Z3, Yices, CVC4) were able to verify all VCs > for the first one, yet the second had a number of VCs that no prover > could discharge. > > I'm curious if this might be some sort of bug in Jessie or Frama-C, or > are our provers just weak at dealing with bits? Not a bug, but rather a missing feature: Jessie/Why3 does not send any information about the bitwise-or operator to the provers, so the proof obligations are not provable. That said, your other assumption was right nonetheless. Provers, while not weak at dealing with bits (most of them natively support bitvectors), tend to be weak when mixing bitvector and integer arithmetics. By the way, they are also weak at nonlinear arithmetic, hence your troubles when you tried non-constant rotations. Best regards, Guillaume