[L13]             float x = __VERIFIER_nondet_float();
       VAL        [x=NaN]
[L14]  COND TRUE  x != x
[L15]             //@ assert \false;