Verification with floating point

@dwightguth @andreistefanescu please review 
you can just put ```maxFloat(X, Y)``` instead of ```Z``` and eliminate the ensures