(uf-ho) Fatal failure at src/theory/theory_model.cpp:690

[zhendongsu]

Commit: 31242de
OS: Ubuntu 18.04
Possibly related: #5371

[775] % cvc4 --strings-exp --uf-ho -q small.smt2
Fatal failure within void cvc5::theory::TheoryModel::assignFunctionDefinition(cvc5::Node, cvc5::Node) at /local/suz-local/software/CVC4/src/theory/theory_model.cpp:690
Check failure

 f_def.isConst()
Non-constant f_def: (lambda (($x1 b) ($x2 b)) (let ((_let_1 (h (h e)))) (ite (and (= _let_1 $x1) (= _let_1 $x2)) (h _let_1) e)))
Aborted
[776] % 
[776] % cat small.smt2
(declare-datatypes ((a 0) (b 0)) (((c) (d)) ((h (j b)) (e))))
(declare-fun f () b)
(declare-fun k (a) b)
(declare-fun g (b b) b)
(assert (forall ((i a)) (distinct (k i) (ite ((_ is c) i) e (ite ((_ is d) i) (h (g (k  i) (k  i))) f)))))
(check-sat)
[777] % 

[HanielB]

This issue no longer occurs. Probably fixed by #6697, which improved the interplay between the HOL setup and the rest of the solver (particularly with --strings-exp).

[HanielB]

The failure is still triggered in debug.