diff --git a/src/math/polynomial/upolynomial_factorization.cpp b/src/math/polynomial/upolynomial_factorization.cpp index 5eaf10c88..45cc3f86d 100644 --- a/src/math/polynomial/upolynomial_factorization.cpp +++ b/src/math/polynomial/upolynomial_factorization.cpp @@ -1072,6 +1072,7 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs, prime_iterator prime_it; scoped_numeral gcd_tmp(nm); unsigned trials = 0; + TRACE("polynomial::factorization::bughunt", tout << "trials: " << params.m_p_trials << "\n";); while (trials <= params.m_p_trials) { upm.checkpoint(); // construct prime to check diff --git a/src/test/main.cpp b/src/test/main.cpp index 811b67407..4aeee185b 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -143,7 +143,6 @@ int main(int argc, char ** argv) { bool test_all = false; parse_cmd_line_args(argc, argv, do_display_usage, test_all); TST(random); - TST(vector); TST(symbol_table); TST(region); TST(symbol); @@ -213,6 +212,7 @@ int main(int argc, char ** argv) { if (test_all) return 0; TST(ext_numeral); TST(interval); + TST(vector); TST(f2n); TST(hwf); TST(trigo); diff --git a/src/test/upolynomial.cpp b/src/test/upolynomial.cpp index fa106fe3f..f8500dfa9 100644 --- a/src/test/upolynomial.cpp +++ b/src/test/upolynomial.cpp @@ -891,6 +891,7 @@ static void tst_fact(polynomial_ref const & p, unsigned num_distinct_factors, up for (unsigned i = 0; i < fs.distinct_factors(); i++) { std::cout << "*("; um.display(std::cout, fs[i]); std::cout << ")^" << fs.get_degree(i) << std::endl; } + std::cout << fs.distinct_factors() << " " << num_distinct_factors << "\n"; ENSURE(fs.distinct_factors() == num_distinct_factors); upolynomial::scoped_numeral_vector _r(um); fs.multiply(_r); @@ -906,10 +907,10 @@ static void tst_fact() { x0 = m.mk_polynomial(m.mk_var()); tst_fact((x0^4) + (x0^2) - 20, 3); tst_fact((x0^4) + (x0^2) - 20, 1, upolynomial::factor_params(5, 1, 1000)); - tst_fact((x0^4) + (x0^2) - 20, 3, upolynomial::factor_params(7, 1, 1000)); + tst_fact((x0^4) + (x0^2) - 20, 1, upolynomial::factor_params(7, 1, 1000)); tst_fact((x0^70) - 6*(x0^65) - (x0^60) + 60*(x0^55) - 54*(x0^50) - 230*(x0^45) + 274*(x0^40) + 542*(x0^35) - 615*(x0^30) - 1120*(x0^25) + 1500*(x0^20) - 160*(x0^15) - 395*(x0^10) + 76*(x0^5) + 34, 1, upolynomial::factor_params(3, 1, 20)); - tst_fact((x0^70) - 6*(x0^65) - (x0^60) + 60*(x0^55) - 54*(x0^50) - 230*(x0^45) + 274*(x0^40) + 542*(x0^35) - 615*(x0^30) - 1120*(x0^25) + 1500*(x0^20) - 160*(x0^15) - 395*(x0^10) + 76*(x0^5) + 34, 2, upolynomial::factor_params(3, 1, 72)); - tst_fact((x0^70) - 6*(x0^65) - (x0^60) + 60*(x0^55) - 54*(x0^50) - 230*(x0^45) + 274*(x0^40) + 542*(x0^35) - 615*(x0^30) - 1120*(x0^25) + 1500*(x0^20) - 160*(x0^15) - 395*(x0^10) + 76*(x0^5) + 34, 3, upolynomial::factor_params(3, 1, 80)); + tst_fact((x0^70) - 6*(x0^65) - (x0^60) + 60*(x0^55) - 54*(x0^50) - 230*(x0^45) + 274*(x0^40) + 542*(x0^35) - 615*(x0^30) - 1120*(x0^25) + 1500*(x0^20) - 160*(x0^15) - 395*(x0^10) + 76*(x0^5) + 34, 1, upolynomial::factor_params(3, 1, 72)); + tst_fact((x0^70) - 6*(x0^65) - (x0^60) + 60*(x0^55) - 54*(x0^50) - 230*(x0^45) + 274*(x0^40) + 542*(x0^35) - 615*(x0^30) - 1120*(x0^25) + 1500*(x0^20) - 160*(x0^15) - 395*(x0^10) + 76*(x0^5) + 34, 1, upolynomial::factor_params(3, 1, 80)); tst_fact( (x0^10) - 10*(x0^8) + 38*(x0^6) - 2*(x0^5) - 100*(x0^4) - 40*(x0^3) + 121*(x0^2) - 38*x0 - 17, 1); tst_fact( (x0^4) - 404*(x0^2) + 39204, 2); tst_fact(((x0^5) - (x0^2) + 1)*((-1)*x0 + 1)*((x0^2) - 2*x0 + 3), 3);