This patch moves the last method in Z3ConstraintManager to SMTConstraintManager: canReasonAbout().
The canReasonAbout() method checks if a given SVal can be encoded in SMT. I've added a new method to the SMT API to return true if a solver can encode floating-point arithmetics and it was enough to make canReasonAbout() solver independent.
As an annoying side-effect, Z3ConstraintManager is pretty empty now and only (1) creates the Z3 solver object by calling CreateZ3Solver() and (2) instantiates SMTConstraintManager. Maybe we can get rid of this class altogether in the future: a CreateSMTConstraintManager() method that does (1) and (2) and returns the constraint manager object?