From a8318b8822da5d56f0859a9fdc84196e2a3e3984 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 19 Dec 2017 09:38:35 -0500 Subject: [PATCH] Fix lemma::has_binding() --- src/muz/spacer/spacer_context.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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);