Encoding RTL Constructs for MathSAT: a Preliminary Report