mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

Debug prints

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-27 22:42:19 -04:00
parent 7c924c49f6
commit 0e5434ce0c
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/muz/spacer/spacer_context.cpp
View file

@ -279,6 +279,8 @@ pob *derivation::create_next_child(model &mdl)
m_evars.reset(); m_evars.reset();
pt().mbp(vars, m_trans, mdl, pt().mbp(vars, m_trans, mdl,
true, pt().get_context().use_ground_pob()); true, pt().get_context().use_ground_pob());
CTRACE("spacer", !vars.empty(),
tout << "Failed to eliminate: " << vars << "\n";);
m_evars.append (vars); m_evars.append (vars);
vars.reset(); vars.reset();
} }
@ -308,6 +310,8 @@ pob *derivation::create_next_child(model &mdl)
vars.append(m_evars); vars.append(m_evars);
pt().mbp(vars, post, mdl, pt().mbp(vars, post, mdl,
true, pt().get_context().use_ground_pob()); true, pt().get_context().use_ground_pob());
CTRACE("spacer", !vars.empty(),
tout << "Failed to eliminate: " << vars << "\n";);
//qe::reduce_array_selects (*mev.get_model (), post); //qe::reduce_array_selects (*mev.get_model (), post);
} }
else { else {
@ -411,6 +415,8 @@ pob *derivation::create_next_child ()
this->pt().mbp(vars, m_trans, *mdl, this->pt().mbp(vars, m_trans, *mdl,
true, this->pt().get_context().use_ground_pob()); true, this->pt().get_context().use_ground_pob());
// keep track of implicitly quantified variables // keep track of implicitly quantified variables
CTRACE("spacer", !vars.empty(),
tout << "Failed to eliminate: " << vars << "\n";);
m_evars.append (vars); m_evars.append (vars);
vars.reset(); vars.reset();
} }