We show how to apply a non-disjoint extension of the Nelson-Oppen
combination method to develop a decision procedure for the union of
theories sharing some arithmetic operators. Different possible
shared theories are discussed: two possible axiomatisations for
counter arithmetic, and the theory of abelian groups. We present
theories modelling some data-structures for which the combination
method is complete and effective. To achieve effectiveness, the
combination method relies on particular procedures to compute sets
that are representative of all the consequences over the shared
theory. We show how to compute these sets by using an appropriate
superposition calculus and a careful adaptation of standard methods
for reasoning about arithmetic. We discuss the underlying
implementation issues and the possible integration of the
non-disjoint combination method into a SMT solver.