Project

General

Profile

Download (219 Bytes)

Bug #3488 » rec.c

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

    (1-1/1)