mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

fix bugs reported by Arie Gurfinkel

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-08-15 18:36:27 -07:00
parent 8f515ef356
commit 01d59d2c91
2 changed files with 11 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/muz_qe/pdr_context.cpp
View file

@ -1881,6 +1881,11 @@ namespace pdr {
// predicate transformer (or some unfolding of it).
//
lbool context::expand_state(model_node& n, expr_ref_vector& result, bool& uses_level) {
TRACE("pdr",
tout << "expand_state: " << n.pt().head()->get_name();
tout << " level: " << n.level() << "\n";
tout << mk_pp(n.state(), m) << "\n";);
return n.pt().is_reachable(n, &result, uses_level);
}

11
src/muz_qe/pdr_generalizers.cpp
View file

@ -195,13 +195,14 @@ namespace pdr {
}
conv1.append(eqs);
if (m_is_closure) {
conv1.push_back(a.mk_gt(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real())));
conv1.push_back(a.mk_gt(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real())));
}
else {
conv1.push_back(a.mk_ge(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real())));
conv1.push_back(a.mk_ge(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real())));
}
else {
// is interior:
conv1.push_back(a.mk_gt(m_sigma[0].get(), a.mk_numeral(rational(0), a.mk_real())));
conv1.push_back(a.mk_gt(m_sigma[1].get(), a.mk_numeral(rational(0), a.mk_real())));
}
conv1.push_back(m.mk_eq(a.mk_numeral(rational(1), a.mk_real()), a.mk_add(m_sigma[0].get(), m_sigma[1].get())));
expr_ref fml = n.pt().get_formulas(n.level(), false);
expr_ref_vector fmls(m);
@ -235,7 +236,7 @@ namespace pdr {
verbose_stream() << "Generalized to:\n" << mk_pp(state1, m) << "\n";);
}
}
if (!m_is_closure || new_cores.empty()) {
if (!m_is_closure || new_cores.size() == orig_size) {
new_cores.push_back(std::make_pair(core, uses_level));
}