$z3 bug.smt2
[1]    114331 segmentation fault  solver_binaries/z3/build-2020-02-24-238ff78/z3 bug.smt2
$cat bug.smt2 
(declare-fun e () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun k () Real)
(declare-fun c () Real)
(declare-fun n () Real)
(declare-fun a () Real)
(declare-fun j () Real)
(declare-fun r () Real)
(declare-fun f () Real)
(declare-fun l () Real)
(declare-fun s () Real)
(declare-fun d () Real)
(declare-fun u () Real)
(declare-fun m () Real)
(declare-fun o () Real)
(declare-fun p () Real)
(declare-fun b () Real)
(declare-fun aa () Real)
(declare-fun q () Real)
(declare-fun ab () Real)
(declare-fun t () Real)
(assert
 (forall ((i Real))
  (let ((v (and (= m g) (= l (/ 0 u)) (distinct (/ d s) 1.0)))
        (w (or (< 0.0 i) (>= i (- c))))
        (x (> 0.0 (* (/ 0.0 k) h))))
   (and (or v (>= (/ 3.0 k) l) (<= (/ f r) 0.0))
    (> j g) (< 0.0 (/ a n)) (> 0.0 g) w (or x (< (- h) g) (< 0.0 e))))))
(assert
 (exists ((c Real))
  (let ((v (>= (/ 5.0 b m) n o))
        (w (/ (* ab g (/ 0 g)) p))
        (x (- (+ (/ 166.0 aa h) (* 5.0 r r))
            (- (- 250.0 (/ 100.0 r)) (+ 120.0 b))))
        (y (+ 115.0 (/ 155.0 (+ 199.0 aa h) (- 197.0 r r))
            (/ (* 2.0 r) (/ 253.0 b m)) (- 73.0 q)))
        (z (* (+ (/ 8.0 aa h) r) b m)))
   (let ((ac (>= o (* 29.0 123.0 (- (+ x 24.0 q)))))
         (ad (/ (* (/ 8.0 (- h)) b m) z)))
    (let ((ae (>= (/ 3.5 y (* ad p)) o)))
     (or (and (or (> 0.0 r) v) (>= w (/ aa h))) (and ac ae)))))))
(assert (distinct b (+ m t g)))
(check-sat)