Verification with floating point

@dwightguth @andreistefanescu please review 
Yeah, but the semantics of "=/=Float" should be the same as ```distinct``` in z3, right?