From 51a5d22f238818e8166148f0974ae6aa63cae8d2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 2 Jan 2013 09:50:31 -0800 Subject: [PATCH] experiments wtih QHC Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_context.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 5784c7be2..5581732c8 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -1206,11 +1206,7 @@ namespace datalog { for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { ptr_vector sorts; get_free_vars(m_rule_fmls[i].get(), sorts); - while (!sorts.empty() && !sorts.back()) { - sorts.pop_back(); - } if (!sorts.empty()) { - std::cout << "has free vars " << mk_pp(m_rule_fmls[i].get(), m) << "\n"; rm.mk_rule(m_rule_fmls[i].get(), rule_refs, m_rule_names[i]); m_rule_fmls[i] = m_rule_fmls.back(); m_rule_names[i] = m_rule_names.back();