From 98d86c6687cad51c6780e403300d4160c79ba0cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Jun 2025 08:08:10 -0700 Subject: [PATCH] disable tracing in test code Signed-off-by: Nikolaj Bjorner --- src/test/algebraic.cpp | 4 ++-- src/test/ddnf.cpp | 2 +- src/test/egraph.cpp | 2 +- src/test/euf_arith_plugin.cpp | 2 +- src/test/euf_bv_plugin.cpp | 4 ++-- src/test/heap.cpp | 1 - src/test/mpf.cpp | 2 +- src/test/mpff.cpp | 4 ++-- src/test/polynomial.cpp | 24 ++++++++++++------------ src/test/quant_elim.cpp | 10 +++++----- src/test/rcf.cpp | 6 +++--- src/test/theory_pb.cpp | 2 +- src/test/upolynomial.cpp | 12 ++++++------ 13 files changed, 37 insertions(+), 38 deletions(-) diff --git a/src/test/algebraic.cpp b/src/test/algebraic.cpp index 8d1b60777..ba219ce9b 100644 --- a/src/test/algebraic.cpp +++ b/src/test/algebraic.cpp @@ -336,7 +336,7 @@ static void tst_eval_sign(polynomial_ref const & p, anum_manager & am, } static void tst_eval_sign() { - enable_trace("anum_eval_sign"); + // enable_trace("anum_eval_sign"); reslimit rl; unsynch_mpq_manager qm; polynomial::manager pm(rl, qm); @@ -417,7 +417,7 @@ static void tst_isolate_roots(polynomial_ref const & p, anum_manager & am, } static void tst_isolate_roots() { - enable_trace("isolate_roots"); + // enable_trace("isolate_roots"); reslimit rl; unsynch_mpq_manager qm; polynomial::manager pm(rl, qm); diff --git a/src/test/ddnf.cpp b/src/test/ddnf.cpp index c62adb4f9..d91a10397 100644 --- a/src/test/ddnf.cpp +++ b/src/test/ddnf.cpp @@ -201,7 +201,7 @@ void tst_ddnf(char ** argv, int argc, int& i) { } void tst_ddnf1() { - enable_trace("ddnf"); + // enable_trace("ddnf"); unsigned W = 2; datalog::ddnf_core ddnf(W); tbv_manager& tbvm = ddnf.get_tbv_manager(); diff --git a/src/test/egraph.cpp b/src/test/egraph.cpp index a3e70a77f..916d7e18a 100644 --- a/src/test/egraph.cpp +++ b/src/test/egraph.cpp @@ -131,7 +131,7 @@ static void test3() { } void tst_egraph() { - enable_trace("euf"); + // enable_trace("euf"); test3(); test1(); test2(); diff --git a/src/test/euf_arith_plugin.cpp b/src/test/euf_arith_plugin.cpp index d8ad15233..ccbae4425 100644 --- a/src/test/euf_arith_plugin.cpp +++ b/src/test/euf_arith_plugin.cpp @@ -99,7 +99,7 @@ static void test3() { } void tst_euf_arith_plugin() { - enable_trace("plugin"); + // enable_trace("plugin"); test1(); test2(); test3(); diff --git a/src/test/euf_bv_plugin.cpp b/src/test/euf_bv_plugin.cpp index ea24ffa5d..a0a1a7f12 100644 --- a/src/test/euf_bv_plugin.cpp +++ b/src/test/euf_bv_plugin.cpp @@ -170,8 +170,8 @@ static void test6() { void tst_euf_bv_plugin() { - enable_trace("bv"); - enable_trace("plugin"); + // enable_trace("bv"); + // enable_trace("plugin"); test6(); return; test1(); diff --git a/src/test/heap.cpp b/src/test/heap.cpp index 402db8934..3f248866d 100644 --- a/src/test/heap.cpp +++ b/src/test/heap.cpp @@ -136,7 +136,6 @@ static void tst2() { void tst_heap() { // enable_debug("heap"); - enable_trace("heap"); unsigned i = 0; while (i < 3) { IF_VERBOSE(1, verbose_stream() << "test\n";); diff --git a/src/test/mpf.cpp b/src/test/mpf.cpp index 6e3dfb67f..c87fafb1e 100644 --- a/src/test/mpf.cpp +++ b/src/test/mpf.cpp @@ -82,7 +82,7 @@ static void bug_set_double() { } void tst_mpf() { - enable_trace("mpf_mul_bug"); + // enable_trace("mpf_mul_bug"); bug_set_int(); bug_set_double(); } diff --git a/src/test/mpff.cpp b/src/test/mpff.cpp index 3dba5d90c..0fcdb27b3 100644 --- a/src/test/mpff.cpp +++ b/src/test/mpff.cpp @@ -610,8 +610,8 @@ static void tst_div(unsigned prec) { } void tst_mpff() { - disable_trace("mpff"); - enable_trace("mpff_trace"); + // disable_trace("mpff"); + // enable_trace("mpff_trace"); // enable_trace("mpff_bug"); // enable_trace("mpff_to_mpq"); // diff --git a/src/test/polynomial.cpp b/src/test/polynomial.cpp index c8a545fc6..320c3e929 100644 --- a/src/test/polynomial.cpp +++ b/src/test/polynomial.cpp @@ -1599,9 +1599,9 @@ static void tst_gcd2() { #if 0 static void tst_gcd3() { - enable_trace("polynomial_gcd"); - enable_trace("polynomial_gcd_detail"); - enable_trace("mpzzp"); + // enable_trace("polynomial_gcd"); + // enable_trace("polynomial_gcd_detail"); + // enable_trace("mpzzp"); polynomial::numeral_manager nm; reslimit rl; polynomial::manager m(rl, nm); polynomial_ref x(m); @@ -1625,7 +1625,7 @@ static void tst_gcd3() { } static void tst_gcd4() { - enable_trace("mgcd"); + // enable_trace("mgcd"); // enable_trace("CRA"); polynomial::numeral_manager nm; reslimit rl; polynomial::manager m(rl, nm); @@ -1817,9 +1817,9 @@ void tst_polynomial() { // enable_trace("factor"); // enable_trace("poly_bug"); // enable_trace("factor_bug"); - disable_trace("polynomial"); - enable_trace("psc_chain_classic"); - enable_trace("Lazard"); + // disable_trace("polynomial"); + // enable_trace("psc_chain_classic"); + // enable_trace("Lazard"); // enable_trace("eval_bug"); // enable_trace("mgcd"); tst_psc(); @@ -1853,11 +1853,11 @@ void tst_polynomial() { // enable_trace("mpz_gcd"); tst_vars(); tst_sqf(); - enable_trace("resultant"); - enable_trace("psc"); - disable_trace("polynomial"); - enable_trace("pseudo_remainder"); - enable_trace("resultant_bug"); + // enable_trace("resultant"); + // enable_trace("psc"); + // disable_trace("polynomial"); + // enable_trace("pseudo_remainder"); + // enable_trace("resultant_bug"); tst_sqrt(); tst_prem(); tst_compose(); diff --git a/src/test/quant_elim.cpp b/src/test/quant_elim.cpp index 8fd5416a1..a505006a2 100644 --- a/src/test/quant_elim.cpp +++ b/src/test/quant_elim.cpp @@ -18,12 +18,12 @@ static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char cons // enable_trace("bit2int"); //enable_trace("gomory_cut"); - enable_trace("final_check_arith"); - enable_trace("arith_final_check"); + // enable_trace("final_check_arith"); + // enable_trace("arith_final_check"); //enable_trace("arith_branching"); - enable_trace("theory_arith_int"); - enable_trace("presburger"); - enable_trace("quant_elim"); + // enable_trace("theory_arith_int"); + // enable_trace("presburger"); + // enable_trace("quant_elim"); // enable_trace("arith_simplifier_plugin"); // enable_trace("non_linear"); // enable_trace("gomory_cut_detail"); diff --git a/src/test/rcf.cpp b/src/test/rcf.cpp index 9b98d9e83..c9fdc49b7 100644 --- a/src/test/rcf.cpp +++ b/src/test/rcf.cpp @@ -71,7 +71,7 @@ static void tst1() { } static void tst2() { - enable_trace("mpz_matrix"); + // enable_trace("mpz_matrix"); unsynch_mpq_manager nm; small_object_allocator allocator; mpz_matrix_manager mm(nm, allocator); @@ -164,8 +164,8 @@ static void tst_denominators() { } void tst_rcf() { - enable_trace("rcf_clean"); - enable_trace("rcf_clean_bug"); + // enable_trace("rcf_clean"); + // enable_trace("rcf_clean_bug"); tst_denominators(); tst1(); tst2(); diff --git a/src/test/theory_pb.cpp b/src/test/theory_pb.cpp index 224578003..240f276e5 100644 --- a/src/test/theory_pb.cpp +++ b/src/test/theory_pb.cpp @@ -47,7 +47,7 @@ public: } void fuzz() { - enable_trace("pb"); + // enable_trace("pb"); unsigned nr = 0; for (unsigned i = 0; i < 100000; ++i) { fuzz_round(nr, 2); diff --git a/src/test/upolynomial.cpp b/src/test/upolynomial.cpp index df7154b42..d6a643a65 100644 --- a/src/test/upolynomial.cpp +++ b/src/test/upolynomial.cpp @@ -1060,10 +1060,10 @@ static void tst_lower_bound() { void tst_upolynomial() { set_verbosity_level(1000); - enable_trace("mpz_gcd"); - enable_trace("normalize_bug"); - enable_trace("factor_bug"); - enable_trace("factor"); + // enable_trace("mpz_gcd"); + // enable_trace("normalize_bug"); + // enable_trace("factor_bug"); + // enable_trace("factor"); // enable_trace("mpzp_inv_bug"); // enable_trace("mpz"); tst_gcd(); @@ -1080,8 +1080,8 @@ void tst_upolynomial() { tst_isolate_roots(); tst_sturm2(); tst_convert_q2bq(); - enable_trace("div_bug"); - enable_trace("mpbq_bug"); + // enable_trace("div_bug"); + // enable_trace("mpbq_bug"); tst_translate_q(); tst_refine(); tst_refinable();