mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

Bugfix for ackermann helper

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-04-08 17:20:09 +01:00
parent bd0bd08ecf
commit 16e487b32a
1 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ackermannization/ackr_helper.h
View file

@ -33,9 +33,13 @@ class ackr_helper {
which are not marked as uninterpreted but effectively are. which are not marked as uninterpreted but effectively are.
*/ */
inline bool should_ackermannize(app const * a) const { inline bool should_ackermannize(app const * a) const {
if (is_uninterp(a))
return true;
else {
decl_plugin * p = m_bvutil.get_manager().get_plugin(a->get_family_id()); decl_plugin * p = m_bvutil.get_manager().get_plugin(a->get_family_id());
return p->is_considered_uninterpreted(a->get_decl()); return p->is_considered_uninterpreted(a->get_decl());
} }
}
inline bv_util& bvutil() { return m_bvutil; } inline bv_util& bvutil() { return m_bvutil; }