Debug branch: Segmentation fault 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)
(declare-fun i () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun p () Real)
(assert (forall ((j Real)) (distinct (<= e 0) (distinct (<= j 0) (<= 0 (+ (* a j) c) (+ (* (/ 100 a 0) j)) e)))))
(assert (exists ((k Real)) (=> (and (<= 0 h) (>= 0 h) (= c 1 l) (= d 0 p) (< 0 i)) (< 0 f))))
(assert (= a m))
(assert (= b (mod p g)))
(check-sat)

Z3 debug branch throws out a segmentation fault:

[709] % z3 small.smt2
unknown
[710] % z3debug small.smt2
Segmentation fault
[711] % 
[711] % cat small.smt2
(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)
(declare-fun i () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun p () Real)
(assert (forall ((j Real)) (distinct (<= e 0) (distinct (<= j 0) (<= 0 (+ (* a j) c) (+ (* (/ 100 a 0) j)) e)))))
(assert (exists ((k Real)) (=> (and (<= 0 h) (>= 0 h) (= c 1 l) (= d 0 p) (< 0 i)) (< 0 f))))
(assert (= a m))
(assert (= b (mod p g)))
(check-sat)
[712] 

OS: Ubuntu 18.04
Commit: a02d3e9

[levnach]

It does not crash anymore, dosed not finish either.