We make a number of contributions to the understanding and practical resolution of quantified constraints. Unlike previous work in the CP literature which was essentially focused on constraints expressed as binary tables, we focus on Presburger Arithmetics, i.e. Boolean combinations of linear constraints. We explain why we think this language is especially interesting. From a theoretical perspective, we clarify the problem of the treatement of universal quantifiers by proposing a “symmetric” version of the notion of quantified consistency. This notion imposes to maintain two constraint stores, which will be used to reason on universal and existential variables, respectively. We then describe an implementation of a branch & bound solver which integrates both forms of propagation and which is, to the best of our knowledge, the first implementation of a CP solver for this class of quantified constraints.