The lack of automated support is probably the main obstacle to the application of formal method techniques in the industrial setting. A possible solution to this problem is to combine the expressiveness of general purpose reasoners (such as theorem provers) with the efficiency of specialized ones (such as decision procedures). This is witnessed by the fact that many theorem provers developed for verification purposes (such as Acl2 [11], PVS [17], Simplify [9], STeP [14], and Tecton [10]) have integrated procedures for ubiquitous theories such as the theory of equality, decidable fragments of arithmetics, lists, and arrays. Unfortunately, designing an effective integration is far from being a trivial task and the solutions available in the verification systems listed above are not completely satisfactory for two main reasons. First, the schemes designed to incorporate decision procedure in larger systems are not flexible enough to allow developers to easily incorporate new procedures. Second, only a tiny portion of the proof obligations arising in many practical applications falls exactly into the domain the specialized reasoners are designed to solve. Thus, in many cases, available decision procedures are of little help if they are not combined with mechanisms for widening their scope.