mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

update func_interp code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-04-18 17:31:36 -07:00
parent 3a6218ac21
commit b512212d41
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/model/func_interp.cpp
View file

@ -113,7 +113,7 @@ bool func_interp::is_fi_entry_expr(expr * e, ptr_vector<expr> & args) {
}
if ((m_arity == 0) ||
(m_arity == 1 && !m().is_eq(c, a1, a2)) ||
(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;