Encoding RTL Constructs for Mathsat: A preliminary report