float-no-simp3_true-unreach-call_true-termination.i

extern void __VERIFIER_error(void);

int main()
{

  float fs1=2.0f/6.0f;
  float fs2=fs1*6.0f;
  if(!((int)fs2==2)) __VERIFIER_error();
}