From fb947f50fbee5d136a5a180358984a29f1c9076a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 26 Nov 2012 20:47:09 -0800 Subject: [PATCH] fold properties at level infty into the other properties as suggested by Arie Signed-off-by: Nikolaj Bjorner --- src/muz_qe/pdr_context.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index d5b495305..9eda8a55e 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -299,6 +299,7 @@ namespace pdr { if (!m_invariants.contains(lemma)) { TRACE("pdr", tout << "property1: " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";); m_invariants.push_back(lemma); + m_prop2level.insert(lemma, lvl); m_solver.add_formula(lemma); return true; } @@ -709,11 +710,6 @@ namespace pdr { for (; it != end; ++it) { add_property(it->m_key, it->m_value); } - for (unsigned i = 0; i < other.m_invariants.size(); ++i) { - expr* e = other.m_invariants[i].get(); - m_invariants.push_back(e); - m_solver.add_formula(e); - } } // ----------------