diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 6f9f4e967..18b017c95 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -1660,7 +1660,7 @@ namespace pdr {
         bool use_model_generalizer = m_params.get_bool(":use-model-generalizer", false);
  
         pred_transformer& pt = n.pt();
-        model_ref M = n.model_ptr();
+        model_ref M = n.get_model_ptr();
         datalog::rule const& r = pt.find_rule(*M);
         expr* T   = pt.get_transition(r);
         expr* phi = n.state();
diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h
index b83aaa7c3..d01670d6f 100644
--- a/src/muz_qe/pdr_context.h
+++ b/src/muz_qe/pdr_context.h
@@ -195,7 +195,7 @@ namespace pdr {
         ptr_vector<model_node> const& children() { return m_children; }
         pred_transformer& pt() const { return m_pt; }
         model_node* parent() const { return m_parent; }
-        model* model_ptr() const { return m_model.get(); }
+        model* get_model_ptr() const { return m_model.get(); }
         model const&  get_model() const { return *m_model; }
         unsigned index() const;
 
diff --git a/src/muz_qe/pdr_quantifiers.cpp b/src/muz_qe/pdr_quantifiers.cpp
index 1a9a6e0e0..df3938acf 100644
--- a/src/muz_qe/pdr_quantifiers.cpp
+++ b/src/muz_qe/pdr_quantifiers.cpp
@@ -418,7 +418,7 @@ namespace pdr {
         // nodes from leaves that are repeated 
         // inside the search tree don't have models.
         //
-        if (!(&node.get_model())) {
+        if (!node.get_model_ptr()) {
             return;
         }
         m_current_rule = &pt.find_rule(node.get_model());