mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

using sk_lt_proc order instead of ast_lt_proc when creating a lemma

Browse source
This commit is contained in:
Arie Gurfinkel 2017-08-07 11:49:05 +02:00
parent 6cf68bee80
commit 1d478bd8d3
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz/spacer/spacer_context.cpp
View file

@ -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();