add logging for rewriter.flat

Z3Prover · Nov 16, 2020 · 36e40a2 · 36e40a2
1 parent 85a2079
commit 36e40a2
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h
@@ -348,7 +348,10 @@ br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * con
         SASSERT(new_args.size() >= 2);
         result = mk_mul_app(new_args.size(), new_args.c_ptr());
         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;
     }