Non-termination(?) when specifying mod0, div0, and additional rules with quantifiers

[Janno]

The example below does not seem to terminate. Removing either of the three quantified assertions makes z3 terminate, though it still takes several seconds (with some variation depending on which assertion is removed).

(declare-fun b () Int)
(declare-fun a () Int)
(assert (forall ((x Int)) (! (= (mod0 x 0) 0) :pattern ((mod0 x 0)))))
(assert (forall ((x Int)) (! (= (div0 x 0) 0) :pattern ((div0 x 0)))))
 (assert (forall ((x Int) (y Int))
  (! (= (mod (mod x y) y) (mod x y)) :pattern ((mod (mod x y) y)))))
(assert (not (= (mod (+ a b) b) (mod a b))))
(check-sat)

I was assuming that these quantified assertions would be relatively harmless given that they could be rewritten eagerly without increasing the problem size. Is that not the case?