Project

General

Profile

Download (348 Bytes)

Bug #13356 » ex13-change-orig.c

Sepideh Asadi, 26/09/2019 13:47

 

int nondet_int();

int get_even(int a, int b){
int rnd = 0;
if (a > 5 || b < 5){
rnd = a;
} else {
rnd = b;
}
return rnd;
}

int test1(int a){
return get_even(a, 5);
}

int test2(int a){
return get_even(5, a);
}

void main(void)
{

int a = nondet_int();

int a1 = test1(a);
int a2 = test2(a);

assert(a1 == a2);

}
(1-1/2)