Verification with floating point

@dwightguth @andreistefanescu please review 
yes, it's specified at the beginning of page 4 of http://www.cprover.org/SMT-LIB-Float/smt-fpa.pdf.