From 01d59d2c9164d1070d895c9db7f9c78f576e169f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Aug 2013 18:36:27 -0700 Subject: [PATCH] fix bugs reported by Arie Gurfinkel Signed-off-by: Nikolaj Bjorner --- src/muz_qe/pdr_context.cpp | 5 +++++ src/muz_qe/pdr_generalizers.cpp | 11 ++++++----- 2 files changed, 11 insertions(+), 5 deletions(-) diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index fd86a4402..ff40be4f3 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -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); } diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp index bf1693ce3..28226dffa 100644 --- a/src/muz_qe/pdr_generalizers.cpp +++ b/src/muz_qe/pdr_generalizers.cpp @@ -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)); }