mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

fix #1512

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-02 20:14:59 +09:00
parent 00c3f4fdcd
commit a738f5af12
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/model/func_interp.cpp
View file

@ -112,7 +112,8 @@ bool func_interp::is_fi_entry_expr(expr * e, ptr_vector<expr> & 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;