[SMT-LIB] An SMT-Lib logic with fixed-size bit vectors _and_ rationals/floating-point numbers?

[Evgeny Roubinchtein]

Dear friends of SMT-Lib,

For my summer internship here at Mathworks, I am helping evaluate the feasibility of using an off-the-shelf SMT solver as part of automated test generation tool chain (presently, an internally-developed solver is used).
I would like to use SMT-Lib format to interface with the solver (I am presently using CVC4  via its SMT-Lib interface).   We (the folks I am working with here at Mathworks and yours truly) feel that, in order to handle some of our test generation tasks,  we really need to work in a logic that includes _both_ fixed-size bit vectors and some manner of non-integer numbers (either rationals or floating point).  However, such a logic doesn't seem to be part of the standard (http://smtlib.cs.uiowa.edu/logics.shtml).    Does my description of the problem make sense?  If so, would you have some suggestions on possible ways to proceed?

Thank you in advance!

-- 
Best,
Evgeny