diff --git a/src/muz_qe/heap_trie.h b/src/muz_qe/heap_trie.h index 25689e930..de07423b6 100644 --- a/src/muz_qe/heap_trie.h +++ b/src/muz_qe/heap_trie.h @@ -88,7 +88,7 @@ class heap_trie { out << " value: " << m_value; } virtual unsigned num_nodes() const { return 1; } - virtual unsigned num_leaves() const { return ref_count()>0?1:0; } + virtual unsigned num_leaves() const { return this->ref_count()>0?1:0; } }; typedef buffer, true, 2> children_t;