From 30a4a84c7993d38d9e4c7f32bd9d39e054b4a113 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 8 Jul 2026 18:53:51 -0700 Subject: [PATCH] move verbose out to where it is used --- src/smt/smt_quantifier.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 1a1e9a748b..f253f24e5d 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -857,10 +857,8 @@ namespace smt { // Compile HO pattern and also register the compiled version with MAM if (m_ho_matcher) { auto [q1, p1] = m_ho_matcher->compile_ho_pattern(q, mp); - IF_VERBOSE(10, verbose_stream() << "ho_matching: q=" << q->get_qid() - << " compiled=" << (p1 != mp) - << " p1=" << mk_pp(p1, m) << "\n"); if (p1 != mp) { + IF_VERBOSE(10, verbose_stream() << "ho_matching: q=" << q->get_qid() << " p1= " << mk_pp(p1, m) << "\n"); m_lazy_mam->add_pattern(q1, p1); } }