(declare-fun a () Real)  
(declare-fun c () Real)  
(declare-fun b () Real)  
(declare-fun j () Real)   
(declare-fun d () Real)  
(declare-fun k () Real)  
(declare-fun e () Real)  
(declare-fun f () Real)  
(declare-fun i () Real)    
(declare-fun g () Real)  
(declare-fun h () Real)  
(declare-fun o () Real)   
(declare-fun q () Real)  
(declare-fun l () Real)  
(declare-fun m () Real)  
(declare-fun n () Real)   
(declare-fun p () Real)  
(declare-fun u () Real)   
(declare-fun t () Real)  
(declare-fun r () Real)  
(assert (forall ((s Real)) (and (or (= i o (/ 3  r)) (>= e o)  
(<= 0.0 g)) (> 0.0 o) (or (< 0.0 s) (>= s c))  
(or (< 0 o) (< 0 (* k p))  (= f 2.0)))))  
(assert (or (and (or (> 0.0 q) (>= (/ 5 a) u)  (< l n))   
(>= (- (/ (*   o  (/  d o))   m))  0.0 (/ 52 j h) u b)) 
(>= l (* 29 (+ 121 2) (- 183 (- (+ 101 (/ 166 j h) (* 14 q q)) (- 250 (/ 202 2.0 q) (+ 120 a i))) (+ 22 2.0 n)))) 
(>= (/ 7 (* (+ 115 (+ (/ 155 (+ 199 j h) (- 197 q q)) (/ (* 2.0 q) (/ 253 a i))) (- 75 2.0 n))) (* (/ (* 6 (/ 8 (-  j h) q i)) (*  (+ (/ 48 j h)  a i))))) l)))  
(assert (= a (+ i t)))  
(check-sat)  

$ z3/build/z3 small.smt2 
Segmentation fault
$ cat small.smt2
(declare-fun a () Real)  
(declare-fun c () Real)  
(declare-fun b () Real)  
(declare-fun j () Real)   
(declare-fun d () Real)  
(declare-fun k () Real)  
(declare-fun e () Real)  
(declare-fun f () Real)  
(declare-fun i () Real)    
(declare-fun g () Real)  
(declare-fun h () Real)  
(declare-fun o () Real)   
(declare-fun q () Real)  
(declare-fun l () Real)  
(declare-fun m () Real)  
(declare-fun n () Real)   
(declare-fun p () Real)  
(declare-fun u () Real)   
(declare-fun t () Real)  
(declare-fun r () Real)  
(assert (forall ((s Real)) (and (or (= i o (/ 3  r)) (>= e o)  
(<= 0.0 g)) (> 0.0 o) (or (< 0.0 s) (>= s c))  
(or (< 0 o) (< 0 (* k p))  (= f 2.0)))))  
(assert (or (and (or (> 0.0 q) (>= (/ 5 a) u)  (< l n))   
(>= (- (/ (*   o  (/  d o))   m))  0.0 (/ 52 j h) u b)) 
(>= l (* 29 (+ 121 2) (- 183 (- (+ 101 (/ 166 j h) (* 14 q q)) (- 250 (/ 202 2.0 q) (+ 120 a i))) (+ 22 2.0 n)))) 
(>= (/ 7 (* (+ 115 (+ (/ 155 (+ 199 j h) (- 197 q q)) (/ (* 2.0 q) (/ 253 a i))) (- 75 2.0 n))) (* (/ (* 6 (/ 8 (-  j h) q i)) (*  (+ (/ 48 j h)  a i))))) l)))  
(assert (= a (+ i t)))  
(check-sat)