diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 80c21d61c..c7f9f448f 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1303,8 +1303,7 @@ void lemma::update_cube (pob_ref const &p, expr_ref_vector &cube) {
 }
 
 bool lemma::has_binding(app_ref_vector const &binding) {
-    expr *lem = get_expr();
-    unsigned num_decls = to_quantifier(lem)->get_num_decls();
+    unsigned num_decls = m_zks.size();
 
     SASSERT(binding.size() == num_decls);