Antti Hyvärinen, 06/09/2016 09:48
int nondet();
int f (int a ){
if (a < 10)
return f (a + 1);
return a - 10;
}
void main(){
int y = 0;
int x = nondet();
__CPROVER_assume(x > 8 && x < 100);
if (x > 0) y = f (x);
assert (y >= 0);