diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp
index dd6472224..9f4f4e4fe 100644
--- a/src/muz/spacer/spacer_qe_project.cpp
+++ b/src/muz/spacer/spacer_qe_project.cpp
@@ -66,7 +66,6 @@ class peq {
     app_ref             m_peq;      // partial equality application
     app_ref             m_eq;       // equivalent std equality using def. of partial eq
     array_util          m_arr_u;
-    ast_eq_proc         m_eq_proc;  // for checking if two asts are equal
 
 public:
     static const char* PARTIAL_EQ;
@@ -102,7 +101,7 @@ peq::peq (app* p, ast_manager& m):
     VERIFY (is_partial_eq (p));
     SASSERT (m_arr_u.is_array (m_lhs) &&
              m_arr_u.is_array (m_rhs) &&
-             m_eq_proc (m.get_sort (m_lhs), m.get_sort (m_rhs)));
+             ast_eq_proc() (m.get_sort (m_lhs), m.get_sort (m_rhs)));
     for (unsigned i = 2; i < p->get_num_args (); i++) {
         m_diff_indices.push_back (p->get_arg (i));
     }
@@ -121,7 +120,7 @@ peq::peq (expr* lhs, expr* rhs, unsigned num_indices, expr * const * diff_indice
 {
     SASSERT (m_arr_u.is_array (lhs) &&
              m_arr_u.is_array (rhs) &&
-             m_eq_proc (m.get_sort (lhs), m.get_sort (rhs)));
+             ast_eq_proc() (m.get_sort (lhs), m.get_sort (rhs)));
     ptr_vector<sort> sorts;
     sorts.push_back (m.get_sort (m_lhs));
     sorts.push_back (m.get_sort (m_rhs));