mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 19:32:04 +00:00
Code Activity

change debug output

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-26 19:36:16 -07:00
parent 7e705c4854
commit 2f49094d49
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/qe/mbp/mbp_arith.cpp
View file

@ -47,7 +47,6 @@ namespace mbp {
~imp() {} ~imp() {}
void insert_mul(expr* x, rational const& v, obj_map<expr, rational>& ts) { void insert_mul(expr* x, rational const& v, obj_map<expr, rational>& ts) {
// TRACE("qe", tout << "Adding variable " << mk_pp(x, m) << " " << v << "\n";);
rational w; rational w;
if (ts.find(x, w)) if (ts.find(x, w))
ts.insert(x, w + v); ts.insert(x, w + v);
@ -362,6 +361,10 @@ namespace mbp {
optdefs2mbpdef(defs, index2expr, real_vars, result); optdefs2mbpdef(defs, index2expr, real_vars, result);
if (m_apply_projection) if (m_apply_projection)
apply_projection(result, fmls); apply_projection(result, fmls);
TRACE("qe",
for (auto [v, t] : result)
tout << v << " := " << t << "\n";
tout << "fmls:" << fmls << "\n";);
return result; return result;
} }