The attached smt query query_14.log is proved in less than 2 seconds with version 4.13.3. When migrating to version 4.15.2, the solver runs forever.

Moreover, is there any particular reason to why Z3 does not converge (even with version 4.13.3) when changing definition (in the attached query)
(define-fun @Int.tdiv ((@x Int)(@y Int)) Int (ite (= 0 @y) 0 (ite (<= 0 @x) (div @x @y) (- (div (- @x) @y)))))
to
(define-fun @Int.tdiv ((@x Int)(@y Int)) Int (ite (= 0 @y) 0 (ite (< @x 0) (- (div (- @x) @y)) (div @x @y))))

Does this has to do with how value analysis (i.e., bound propagation) is encoded in z3 ?