From 3a6218ac21532a7af1621db895458c5606defa47 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 18 Apr 2016 17:30:52 -0700 Subject: [PATCH] update func_interp code Signed-off-by: Nikolaj Bjorner --- src/model/func_interp.cpp | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index 96201d900..4dd9d599f 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -107,25 +107,23 @@ void func_interp::reset_interp_cache() { bool func_interp::is_fi_entry_expr(expr * e, ptr_vector & args) { args.reset(); - expr* c, *t, *f; + expr* c, *t, *f, *a0, *a1; if (!m().is_ite(e, c, t, f)) { return false; } if ((m_arity == 0) || - (m_arity == 1 && (!m().is_eq(c) || to_app(c)->get_num_args() != 2)) || + (m_arity == 1 && !m().is_eq(c, a1, a2)) || (m_arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != m_arity))) return false; args.resize(m_arity, 0); for (unsigned i = 0; i < m_arity; i++) { - expr * ci = (m_arity == 1 && i == 0) ? to_app(c) : to_app(c)->get_arg(i); + expr * ci = (m_arity == 1 && i == 0) ? c : to_app(c)->get_arg(i); - if (!m().is_eq(ci) || to_app(ci)->get_num_args() != 2) + if (!m().is_eq(ci, a0, a1)) return false; - expr * a0 = to_app(ci)->get_arg(0); - expr * a1 = to_app(ci)->get_arg(1); if (is_var(a0) && to_var(a0)->get_idx() == i) args[i] = a1; else if (is_var(a1) && to_var(a1)->get_idx() == i)