main.c

#include <math.h>
#include <assert.h>

float nondet();

int main(void)
{
  float from = nondet();
  __ESBMC_assume(from > 0.0f);
  __ESBMC_assume(!isinf(from));
  __ESBMC_assume(!isnan(from));

  union {
    float a;
    long b;
  } from_union = { .a = from };

  from_union.b++;

  assert(from < from_union.a);
}