mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fold properties at level infty into the other properties as suggested by Arie

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-26 20:47:09 -08:00
parent ff866e86a4
commit fb947f50fb
1 changed files with 1 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/muz_qe/pdr_context.cpp
View file

@ -299,6 +299,7 @@ namespace pdr {
if (!m_invariants.contains(lemma)) { if (!m_invariants.contains(lemma)) {
TRACE("pdr", tout << "property1: " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";); TRACE("pdr", tout << "property1: " << head()->get_name() << " " << mk_pp(lemma, m) << "\n";);
m_invariants.push_back(lemma); m_invariants.push_back(lemma);
m_prop2level.insert(lemma, lvl);
m_solver.add_formula(lemma); m_solver.add_formula(lemma);
return true; return true;
} }
@ -709,11 +710,6 @@ namespace pdr {
for (; it != end; ++it) { for (; it != end; ++it) {
add_property(it->m_key, it->m_value); 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);
}
} }
// ---------------- // ----------------