Project

General

Profile

rec.c

Antti Hyvärinen, 06/09/2016 09:48

 
1
int nondet();
2

    
3
int f (int a ){
4
  if (a < 10)
5
    return f (a + 1);
6
  return a - 10;
7
}
8

    
9
void main(){
10
  int y = 0;
11
  int x = nondet();
12
  __CPROVER_assume(x > 8 && x < 100);
13

    
14
  if (x > 0) y = f (x);
15

    
16
  assert (y >= 0);
17
}
18