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);