Z3 assertion violation on NRA formula

[muchang]

Hi,
For this formula,

(declare-fun a() Real)
(declare-fun b() Real)
(declare-fun c() Real)
(declare-fun d() Real)
(declare-fun e() Real)
(declare-fun f() Real)
(declare-fun g() Real)
(declare-fun h() Real)
(assert (forall ((i Real)) (> (/ 5 (- (+ b 1) i) (+ d e)) (+ c a i))))
(assert (< g (+ d h)))
(assert (< 0 g))
(assert (= d (+ 2 h e)))
(assert (= a (+ 2 f)))
(check-sat)

Z3 throws out an assertion violation:

ASSERTION VIOLATION
File: ../src/smt/theory_arith_core.h
Line: 376
!val.is_one()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Revision: cb600a9