diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index accb45a25..2eb687dae 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -112,7 +112,8 @@ bool func_interp::is_fi_entry_expr(expr * e, ptr_vector & args) { return false; } - if ((m_arity == 0) || + if (!is_ground(t) || + (m_arity == 0) || (m_arity == 1 && !m().is_eq(c, a0, a1)) || (m_arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != m_arity))) return false;