Floating point numbers do not form a field

And here is a C program annotated for the C Bounded Model Checker to find a counterexample of associativity for floats:

    #include <math.h>
    extern float nondet_float(); // works equally well (quick) for double
    int main() {
        float a = nondet_float(), b = nondet_float(), c = 1;
        __CPROVER_assume(isfinite(a) && isfinite(b) && isfinite(c));
        float s1 = (a+b)+c, s2 = a+(b+c);
        __CPROVER_assume(isfinite(s1) && isfinite(s2));
        __CPROVER_assert(s1 == s2, "associativity holds for floats");
    }

http://www.cprover.org/cbmc/

Another simple proof of the non-field-ness of floating point numbers. in this case for the IEEE "double precision" type, that associativity doesn't hold:

    >>> a, b, c = 2 ** -53, 2 ** -53, 1
    >>> (a+b)+c == a+(b+c) # definition of associativity
    False