Barr's covering theorem assert that any Gorthendieck topos can be covered by a Grothendieck topos (even a locale) satisfying the axiom of choice (and hence also the law of excluded middle). Its corrolary is that if one can deduce from geometrical hypothesis $H$ a geometric conclusion $C$ using (AC) and classical logic, then one can deduce $C$ from $H$ in any Grothendieck topos.

The proof of this theorem rely heavily on the axiom of choice (actually on the fact that the topos of sheaf over a boolean locale satisfy the axiom of choice) and hence is not valid in a general elementary topos.

My question is : Is there any know examples of something that can be proved using Barr's theorem (a deduction of geometric conclusion from geometric hypothesis which can be proved using (AC) ) and which is false in some elementary topos (preferably with a natural number object) ?

Also, could you confirm me that the weaker form of barr's theorem "every topos can be covered by a boolean topos" is actualy true also for elementary topos ? (it seems that one can consider the topos of double negation sheaf over the internal frame of nuclei of $\Omega$ in every elementary topos)

Edit : Thinking about Zhen Lin answer and comment I realize that my question was unclear : what I am looking for is an exemple of a geometric theory $H$ possibly stated in the language of some elementary topos, which have a geometric consequence $C$ deducible using the axiom of choice such that $C$ cannot be deduce from $H$ constructively. ie, I'm essentially looking for a proof that barr's theorem can't be constructive. In this situation, the completeness theorem for geometric logic (mentioned in Zhen Lin's comment) does not apply because as the theory $H$ can be stated in an elementary topos it does not mean anything to say that $C$ can be deduced from $H$ in any Grothendieck toposes.