ex21upg2.c
1  

2 
unsigned int nondetUInt(); 
3  
4 
int plus2(int a){ 
5 
return a +2; //a=2..12 
6 
} 
7  
8 
int minus2(int b , int a){ 
9 
a = add(a,b); 
10 
return b  2; 
11 
} 
12  
13 
int add(int a, int b){ 
14 
return a + b;

15 
} 
16  
17 
void main(){

18 
int a = nondetUInt;

19 
int b = nondetUInt;

20 
__CPROVER_assume(a>0);

21 
__CPROVER_assume(a<10);

22  
23 
b = plus2(a); 
24 
b = minus2(b , b); 
25 
assert(a > b); 
26 
} 
27 