Verification with floating point

@dwightguth @andreistefanescu please review 
My advice to you is to map it in z3 to (not (== #1 #2))