sumth60.c
1 
int func1(int a, int b) 

2 
{ 
3 
int m = 1; 
4 
for (int i = 0; i < 3; i++) 
5 
{ 
6 
m = (a*a + b / a) + m; 
7 
} 
8 
if(m >= 1) 
9 
return (m % 2); 
10 
else return (m % 3); 
11 
} 
12  
13 
int func2(int a, int b) 
14 
{ 
15 
int m = 1; 
16 
for (int i = 0; i < 3; i++) 
17 
{ 
18 
m= m + ((a * a) + (b / a)); 
19 
} 
20 
return (m % 2); 
21 
} 
22  
23 
int main()

24 
{ 
25 
unsigned int a = nondet(); 
26 
unsigned int b = nondet(); 
27 
int c = a;

28 
int d = b;

29 
int p = func1( a, b)+func2(a, b);

30 
int q = func1(c, d)+func2(c, d);

31 

32 
assert (p*p >= 0); //claim 1 verified by prop 
33 

34 
assert(p == q); //claim 2 expected to be verified by uf

35 

36 
assert(p  q == 0); //can LRA handle this? 
37 

38 
assert(p + q <= 10);

39 

40 
return 0; 
41 
} 