From 1d478bd8d37719a2e22a2a50c5faa2c29bfdc3c1 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Mon, 7 Aug 2017 11:49:05 +0200 Subject: [PATCH] using sk_lt_proc order instead of ast_lt_proc when creating a lemma --- src/muz/spacer/spacer_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 1ab15ae34..6be4b78a3 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -1787,7 +1787,7 @@ void pob::set_post(expr* post, app_ref_vector const &b) { m_binding.append(b); - std::sort (m_binding.c_ptr(), m_binding.c_ptr() + m_binding.size(), ast_lt_proc()); + std::sort (m_binding.c_ptr(), m_binding.c_ptr() + m_binding.size(), sk_lt_proc()); // skolemize implicit existential quantifier ast_manager &m = get_ast_manager();