mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity

fix bug incorrect clearing of goals during node creation. Issue #777

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-11-19 10:06:16 -08:00
parent a5bae72bdf
commit 2ff5af7d42
3 changed files with 15 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/muz/base/dl_context.cpp
View file

@ -1001,14 +1001,20 @@ namespace datalog {
if (is_quantifier(body)) { if (is_quantifier(body)) {
quantifier* q = to_quantifier(body); quantifier* q = to_quantifier(body);
expr* e = q->get_expr(); expr* e = q->get_expr();
VERIFY(m.is_implies(e, body, e2)); if (m.is_implies(e, body, e2)) {
fml = m.mk_quantifier(false, q->get_num_decls(), fml = m.mk_quantifier(false, q->get_num_decls(),
q->get_decl_sorts(), q->get_decl_names(), q->get_decl_sorts(), q->get_decl_names(),
body); body);
}
else {
fml = body;
}
} }
else { else {
VERIFY(m.is_implies(body, body, e2));
fml = body; fml = body;
if (m.is_implies(body, body, e2)) {
fml = body;
}
} }
queries.push_back(fml); queries.push_back(fml);
} }

6
src/muz/pdr/pdr_context.cpp
View file

@ -895,14 +895,12 @@ namespace pdr {
void model_node::dequeue(model_node*& root) { void model_node::dequeue(model_node*& root) {
TRACE("pdr", tout << this << " " << state() << "\n";); TRACE("pdr", tout << this << " root: " << root << " " << state() << "\n";);
root = 0;
if (!m_next && !m_prev) return; if (!m_next && !m_prev) return;
SASSERT(m_next); SASSERT(m_next);
SASSERT(m_prev); SASSERT(m_prev);
SASSERT(children().empty()); SASSERT(children().empty());
if (this == m_next) { if (this == m_next) {
// SASSERT(root == this);
root = 0; root = 0;
} }
else { else {
@ -975,7 +973,7 @@ namespace pdr {
} }
void model_search::enqueue_leaf(model_node* n) { void model_search::enqueue_leaf(model_node* n) {
TRACE("pdr_verbose", tout << n << " " << n->state() << " goal: " << m_goal << "\n";); TRACE("pdr_verbose", tout << "node: " << n << " " << n->state() << " goal: " << m_goal << "\n";);
SASSERT(n->is_open()); SASSERT(n->is_open());
if (!m_goal) { if (!m_goal) {
m_goal = n; m_goal = n;

1
src/muz/pdr/pdr_dl_interface.cpp
View file

@ -148,6 +148,7 @@ lbool dl_interface::query(expr * query) {
TRACE("pdr", TRACE("pdr",
tout << "rules:\n"; tout << "rules:\n";
m_ctx.display_rules(tout); m_ctx.display_rules(tout);
m_ctx.display_smt2(0, 0, tout);
); );
IF_VERBOSE(2, m_ctx.display_rules(verbose_stream());); IF_VERBOSE(2, m_ctx.display_rules(verbose_stream()););