bv_lemma fails to find quantifier pattern: bit decomposition

Oct 19, 2009 at 6:07 PM
Edited Oct 19, 2009 at 6: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

Coordinator
Nov 26, 2009 at 9:12 AM
This discussion has been copied to a work item. Click here to go to the work item and continue the discussion.
Coordinator
Nov 26, 2009 at 9:17 AM
This discussion has been copied to a work item. Click here to go to the work item and continue the discussion.
Coordinator
Nov 26, 2009 at 9:23 AM

I think that should work and have copied the original post to a work item (http://vcc.codeplex.com/WorkItem/View.aspx?WorkItemId=3480). Please ignore the second post of that kind. Best, Mark