CVC4 --sygus-inference check failure on LIA formula at CVC4/src/theory/theory_model_builder.cpp:65

[muchang]

Hi,
For this formula,

(set-logic ALL)
(declare-fun f (Int) Bool)
(declare-fun g (Int) Bool)
(assert (= f g))
(assert (exists ((x Int)) (f x)))
(check-sat)

CVC4 with --sygus-inference will throw out a check failure:

Fatal failure within bool CVC4::theory::TheoryEngineModelBuilder::isAssignable(CVC4::TNode) at /home/CVC4/src/theory/theory_model_builder.cpp:65
Check failure
 !n.getType().isFunction()
Aborted

OS: Ubuntu 18.04
Revision: 5e2d39c

[ajreynol]

Since this problem involves equality between functions, you should use --uf-ho for this problem. This avoids the assertion failure.

[ajreynol]

Fixed in #3551.