Fatal failure at theory/arith/nonlinear_extension.cpp:2685

[rainoftime]

Hi,
For this formula:

(set-logic QF_NRA)
(declare-fun _substvar_58_ () Bool)
(declare-fun _substvar_59_ () Bool)
(declare-fun _substvar_82_ () Bool)
(set-option :cegqi-si-sol-min-core false)
(set-option :sets-rel-eager false)
(set-option :rewrite-rules true)
(set-option :arith-rewrite-equalities true)
(set-option :new-prop false)
(set-option :sygus-unif false)
(set-option :synth-rr-prep true)
(set-option :nl-ext-split-zero true)
(set-option :nl-ext-rbound true)
(set-option :ut-all-bounded false)
(declare-const v8 Bool)
(declare-const r0 Real)
(declare-const r3 Real)
(declare-const r4 Real)
(declare-const r6 Real)
(declare-const r9 Real)
(assert (or _substvar_82_ v8))
(assert (or (>= 4 r3 0.0) _substvar_59_ _substvar_58_))
(assert (>= 0.0 r0 (/ r9 r6) (- r3) (* 4 r4 r3)))
(assert (distinct 0.0 r6 r0))
(check-sat)

CVC4 incremental mode throws out a fatal failure:

Fatal failure within std::vector<CVC4::NodeTemplate<true> > CVC4::theory::arith::NonlinearExtension::checkMonomialInferResBounds() at /home/peisen/test/tofuzz/CVC4/src/theory/arith/nonlinear_extension.cpp:2685
Check failure

 mv_b_sgn != 0

OS: Ubuntu 16.04
Commit: 7d3df3b