nl-ext-split-zero snorm-infer-eq: fatal failure at src/theory/quantifiers/equality_infer.cpp:144

[muchang]

Hi,
For this formula:

(set-option :nl-ext-split-zero true)
(set-option :snorm-infer-eq true)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (distinct 0 (* a c)))
(assert (= c (- a b)))
(check-sat)

CVC4 throws out a fatal failure:

[556] % cvc4-1.7 --quiet small.smt2
sat
[557] % cvc4 --quiet small.smt2
Fatal failure within void CVC4::theory::quantifiers::EqualityInference::eqNotifyNewClass(CVC4::TNode) at src/theory/quantifiers/equality_infer.cpp:144
Check failure
 !eqci->d_valid.get()
Aborted
[558] % 
[558] % cat small.smt2
(set-option :nl-ext-split-zero true)
(set-option :snorm-infer-eq true)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (distinct 0 (* a c)))
(assert (= c (- a b)))
(check-sat)

OS: Ubuntu 18.04
Commit: ccca2e7

[ajreynol]

See #3955