Fatal failure at conjecture_generator.cpp:2157

[wintered]

cvc4 -q bug.smt2
Fatal failure within void CVC4::theory::quantifiers::TheoremIndex::addTheoremNode(CVC4::TNode, std::vector<CVC4::NodeTemplate<false> >&, std::vector<unsigned int>&, CVC4::TNode) at /home/windomin/cov/comp/.solvers/cvc4/src/theory/quantifiers/conjecture_generator.cpp:2157
Check failure

 d_var[tn].isNull() || d_var[tn] == curr

Aborted
% cat bug.smt2
(set-option :conjecture-gen true)  
(declare-sort b$ 0) 
(declare-sort c$ 0)    
(declare-sort j$ 0) 
(declare-fun d$ () j$)  
(declare-fun k$ (j$) j$) 
(declare-fun d$a () b$) 
(declare-fun e$ (b$) c$) 
(declare-fun l$ (j$) b$) 
(declare-fun g$f (c$ b$) b$)  
(assert (= (g$f (e$ d$a) d$a) (l$ (k$ d$))))
(assert (forall ((?m b$) (?h b$) (?i b$)) (= (= (g$f (e$ ?m) ?h) (g$f (e$ ?i) ?h)) (= ?m ?i)))) 
(assert (forall ((?m b$) (?h b$) (?i b$)) (= (= (g$f (e$ ?m) ?h) (g$f (e$ ?m) ?i)) (= ?h ?i)))) 
(check-sat)

OS: Ubuntu 18.04 Commit: 8476f38

[ajreynol]

conjecture-gen is experimental; it is designed to work only for quantifiers over datatypes.