Verification with floating point

@dwightguth @andreistefanescu please review 
Actually, I can't. ```==Float``` is different from ```=?``` in the prover, which is translated to ```=``` rather than ```==``` in z3.