hifrog

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;

}