I have applied the purify-arith tactic to the
(forall ((x Int)) (= (mod x 3) 0)))
and got this
(forall ((x Int))
(exists ((x!0 Real)) (and (= x!0 0) (<= 0 x) (not (<= 3 x)) (= x 0)))))
It seems strange that the introduced quantifier bounds a real variable. It's not the expected behavior, is it?