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

Debug print

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-21 21:28:50 -07:00
parent efb1f50d00
commit bf4c35982f
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/qe/qe_arrays.cpp
View file

@ -631,13 +631,13 @@ namespace qe {
m_v = arr_vars.get (i); m_v = arr_vars.get (i);
if (!m_arr_u.is_array (m_v)) { if (!m_arr_u.is_array (m_v)) {
TRACE ("qe", TRACE ("qe",
tout << "not an array variable: " << m_v << "\n"; tout << "not an array variable: " << mk_pp (m_v, m) << "\n";
); );
aux_vars.push_back (m_v); aux_vars.push_back (m_v);
continue; continue;
} }
TRACE ("qe", TRACE ("qe",
tout << "projecting equalities on variable: " << m_v << "\n"; tout << "projecting equalities on variable: " << mk_pp (m_v, m) << "\n";
); );
if (project (fml)) { if (project (fml)) {
@ -653,8 +653,8 @@ namespace qe {
); );
} }
else { else {
IF_VERBOSE(2, verbose_stream() << "can't project:" << m_v << "\n";); IF_VERBOSE(2, verbose_stream() << "can't project:" << mk_pp(m_v, m) << "\n";);
TRACE ("qe", tout << "Failed to project: " << m_v << "\n";); TRACE ("qe", tout << "Failed to project: " << mk_pp (m_v, m) << "\n";);
arr_vars[j++] = m_v; arr_vars[j++] = m_v;
} }
} }