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

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/ http://www.cprover.org/cbmc/