#include #include #include #include #include #include #include float nondet_float(); float fn1(float x) { return sqrtf(x); } float fn2(float x) { return sqrtf(x); } int main(void) { float v = nondet_float(); float r1, r2; r1 = fn1(v); r2 = fn2(v); assert(r1 == r2 || (isnan(r1) && isnan(r2))); }