diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index d65960857..25535856e 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -346,14 +346,16 @@ br_status poly_rewriter::mk_nflat_mul_core(unsigned num_args, expr * con SASSERT(sums.back()[0] == arg); } } + unsigned orig_size = sums.size(); expr_ref_buffer sum(m()); // must be ref_buffer because we may throw an exception ptr_buffer m_args; TRACE("som", tout << "starting som...\n";); do { TRACE("som", for (unsigned i = 0; i < it.size(); i++) tout << it[i] << " "; tout << "\n";); - if (sum.size() > m_som_blowup) - throw rewriter_exception("sum of monomials blowup"); + if (sum.size() > m_som_blowup * orig_size) { + return BR_FAILED; + } m_args.reset(); for (unsigned i = 0; i < num_args; i++) { expr * const * v = sums[i]; diff --git a/src/ast/rewriter/poly_rewriter_params.pyg b/src/ast/rewriter/poly_rewriter_params.pyg index 18d1e1dba..7e909d4aa 100644 --- a/src/ast/rewriter/poly_rewriter_params.pyg +++ b/src/ast/rewriter/poly_rewriter_params.pyg @@ -2,7 +2,7 @@ def_module_params(module_name='rewriter', class_name='poly_rewriter_params', export=True, params=(("som", BOOL, False, "put polynomials in som-of-monomials form"), - ("som_blowup", UINT, UINT_MAX, "maximum number of monomials generated when putting a polynomial in sum-of-monomials normal form"), + ("som_blowup", UINT, 10, "maximum increase of monomials generated when putting a polynomial in sum-of-monomials normal form"), ("hoist_mul", BOOL, False, "hoist multiplication over summation to minimize number of multiplications"), ("hoist_cmul", BOOL, False, "hoist constant multiplication over summation to minimize number of multiplications"), ("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor")))