Cesare - a few typos in the FloatingPoints.smt2: floting -> floating hexadeximals -> hexadecimals distintion -> distinction Also, are you considering stipulating (or perhaps suggesting) some standard names (in the logic perhaps) for the most common instances of FloatingPoint, as in (define-sort binary32 ( ) (_ FloatingPoint 8 24))