From 983763213b0207201d9b6b9ede9eb3dd7c4f05ec Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 30 Dec 2024 12:36:47 -0800 Subject: [PATCH] temper verbose output on tabu updates Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_bv_lookahead.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp index 57fa61370..dc8cfcd71 100644 --- a/src/ast/sls/sls_bv_lookahead.cpp +++ b/src/ast/sls/sls_bv_lookahead.cpp @@ -374,7 +374,7 @@ namespace sls { } } else { - IF_VERBOSE(1, verbose_stream() << "tabu " << mk_bounded_pp(a, m) << "\n"); + IF_VERBOSE(3, verbose_stream() << "tabu " << mk_bounded_pp(a, m) << " " << wval(a) << "\n"); has_tabu = true; } } @@ -486,7 +486,7 @@ namespace sls { m_ev.eval(e); // updates wval(e).eval if (!wval(e).commit_eval()) { TRACE("bv", tout << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n"); - IF_VERBOSE(2, verbose_stream() << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n"); + IF_VERBOSE(3, verbose_stream() << "failed to commit " << mk_bounded_pp(e, m) << " " << wval(e) << "\n"); // bv_plugin::is_sat picks up discrepancies continue; }