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

add logging for rewriter.flat

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-11-16 11:20:33 -08:00
parent 85a20791db
commit 36e40a296f
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/rewriter/poly_rewriter_def.h
View file

@ -348,7 +348,10 @@ br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * con
SASSERT(new_args.size() >= 2); SASSERT(new_args.size() >= 2);
result = mk_mul_app(new_args.size(), new_args.c_ptr()); result = mk_mul_app(new_args.size(), new_args.c_ptr());
result = mk_mul_app(c, result); result = mk_mul_app(c, result);
TRACE("poly_rewriter", tout << "mk_nflat_mul_core result:\n" << mk_ismt2_pp(result, m()) << "\n";); TRACE("poly_rewriter",
for (unsigned i = 0; i < num_args; ++i)
tout << mk_ismt2_pp(args[i], m()) << " ";
tout << "\nmk_nflat_mul_core result:\n" << mk_ismt2_pp(result, m()) << "\n";);
return BR_DONE; return BR_DONE;
} }