From 16e487b32a07a3c218cb0f0f76afc9321c9ed37d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 8 Apr 2016 17:20:09 +0100 Subject: [PATCH] Bugfix for ackermann helper --- src/ackermannization/ackr_helper.h | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/ackermannization/ackr_helper.h b/src/ackermannization/ackr_helper.h index 70d6ab57b..327763da4 100644 --- a/src/ackermannization/ackr_helper.h +++ b/src/ackermannization/ackr_helper.h @@ -33,8 +33,12 @@ class ackr_helper { which are not marked as uninterpreted but effectively are. */ inline bool should_ackermannize(app const * a) const { - decl_plugin * p = m_bvutil.get_manager().get_plugin(a->get_family_id()); - return p->is_considered_uninterpreted(a->get_decl()); + if (is_uninterp(a)) + return true; + else { + decl_plugin * p = m_bvutil.get_manager().get_plugin(a->get_family_id()); + return p->is_considered_uninterpreted(a->get_decl()); + } } inline bv_util& bvutil() { return m_bvutil; }