Project

General

Profile

Download (793 Bytes)

Bug #7805 » sumth60.c

Sepideh Asadi, 29/08/2018 13:03

 
int func1(int a, int b)
{
int m = 1;
for (int i = 0; i < 3; i++)
{
m = (a*a + b / a) + m;
}
if(m >= 1)
return (m % 2);
else return (m % 3);
}

int func2(int a, int b)
{
int m = 1;
for (int i = 0; i < 3; i++)
{
m= m + ((a * a) + (b / a));
}
return (m % 2);
}

int main()
{
unsigned int a = nondet();
unsigned int b = nondet();
int c = a;
int d = b;
int p = func1( a, b)+func2(a, b);
int q = func1(c, d)+func2(c, d);
assert (p*p >= 0); //claim 1 verified by prop
assert(p == q); //claim 2 expected to be verified by uf
assert(p - q == 0); //can LRA handle this?
assert(p + q <= 10);
return 0;
}
(1-1/2)