Check failure src/theory/uf/equality_engine.cpp:1162

[wintered]

[585] % cvc4 -q small.smt2
Fatal failure within void CVC4::theory::eq::EqualityEngine::getExplanation(CVC4::theory::eq::EqualityNodeId, CVC4::theory::eq::EqualityNodeId, std::vector<CVC4::NodeTemplate<false> >&, std::map<std::pair<unsigned int, unsigned int>, CVC4::theory::eq::EqProof*>&, CVC4::theory::eq::EqProof*) const at src/theory/uf/equality_engine.cpp:1162
Check failure
 canExplain
Aborted
[586] % 
[586] % cat small.smt2
(set-option :sygus-inference true)
(set-option :use-soi true)
(set-option :arith-rewrite-equalities true)
(set-option :ag-miniscope-quant true)
(set-option :nl-ext-rewrite false)
(set-option :relational-triggers true)
(set-option :snorm-infer-eq true)
(set-option :qcf-tconstraint true)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun aa () Real)
(declare-fun e () Real)
(declare-fun ab () Real)
(declare-fun ac () Real)
(declare-fun ad () Real)
(declare-fun f () Real)
(declare-fun ae () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun af () Real)
(declare-fun az () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun ah () Real)
(declare-fun n () Real)
(declare-fun ai () Real)
(declare-fun o () Real)
(declare-fun aj () Real)
(declare-fun p () Real)
(declare-fun ak () Real)
(declare-fun q () Real)
(declare-fun al () Real)
(declare-fun am () Real)
(declare-fun an () Real)
(declare-fun r () Real)
(declare-fun ao () Real)
(declare-fun v () Real)
(declare-fun w () Real)
(declare-fun s () Real)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(declare-fun ap () Real)
(declare-fun t () Real)
(declare-fun aq () Real)
(declare-fun ar () Real)
(assert (and (forall ((ai Real)) (=> (and (or (or (or (and (and (and
(or (and (and (and (and (and (or (or (= al (- c d)) (= (- 8 w) 0.0))
(= ac 0.0)) (= (+ 203 ac t) 2.0)) (= (- t) 2.0)) (>= (/ ak (+ (+ (/ 82
b (* i ak)) (* b (+ i ak))) (/ 2.0 (/ 12 aa t)))) 0)) (= (/ 14 ae ap)
2.0)) (<= al (/ 3 h ap))) (< 0.0 (/ 14 aa t))) (> 0.0 (- 8 (- 4 i
ak)))) (< (* 7 b) am)) (>= 0.0 (+ e (/ 5 ab ah)))) (<= (* e ah) am))
(<= 0.0 m)) (< 0.0 am)) (>= 0.0 an)) (or (= (/ 10 az t) aq)
(and (<= 0.0 k) (xor (=> (and (>= 0.0 ai) (<= ai k)) (and (or (and (or
(<= 0.0 (/ 8 af w)) (< (- w) am)) (< 0.0 (/ (* m ai) ah))) (>= (+ (+ m
ai) ah) am)) (>= (- ai) an))) (or (= aj 2.0))))))) (forall ((u Real))
(or (or (or (and (and (and (and (or (or (and (and (and (and (or (and
(= (* c l) 2.0) (and (and (< 0.0 (- 2 k) y)))) (< 0.0 y)) (= r x)) (>=
0.0 (- g aj))) (< (+ g aj) z)) (< (* w (- (/ (- 4) g aj))) 0.0)) (= (+
i ak) 2.0)) (<= r ar)) (< 0.0 w)) (<= 0.0 (* ad ai))) (> 0 z)) (> 0.0
v)) (>= 0.0 z)) (>= 0.0 (+ f o))) (and (> r (* 4 (+ (/ (- 20) (+ 8 (/
y y)) (+ (+ 2.0 y) (- 3 g aj))) (/ (* (* v y) (+ 4 aj)) (+ (- v y) (/
33 g aj))) (/ 2.0 w))) r))))))
(assert (= b (+ (- 50) j s)))
(assert (= c (+ (- 7) l ap)))
(assert (= d (/ m ap)))
(assert (= ac (/ 78 n t)))
(assert (= g (- aj ao)))
(assert (= h (/ p ap)))
(assert (distinct i (* ak s)))
(assert (= af (/ q w)))
(check-sat)
[587] %

OS: Ubuntu 18.04 Commit: 92ed768

[ajreynol]

snorm-infer-eq no longer exists.