Oct 19, 2009 at 7:07 PM
Edited Oct 19, 2009 at 7:08 PM

Hi all!
for the verification some product code i would need a lemma concerning integer equality on the bit level. Normal assertion fails so i tried bv_lemma which also failed but with the warning ""Prover warning: failed to find a pattern for quantifier
(quantifier id: bvdecomp.5:37)". Please, see the example below. I'm particularly interested in the first lemma.
#include "vcc.h"
void main()
{
bv_lemma(forall(unsigned int a,b; forall(unsigned int j;(j < 32) ==> ((a & (1UL << j)) == (b & (1UL << j)))) ==> (a == b)));
bv_lemma(forall(unsigned int a,b; forall(unsigned int j;(j < 32) ==> ((a & (1UL << j)) == (b & (1UL << j)))) <== (a == b)));
}
the reverse direction verifies with a warning "Prover warning: pulled nested quantifier to be able to find an useable pattern (quantifier id: bvdecomp.6:37)" so maybe the problem is that there is nothing between the two quantifiers.
Is this a Z3 issue? or does anyone have some idea for a workaround in VCC?
thanks,
Christoph
