From a2f5a5b50b47f64ee02db964058da05ce00a4656 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 5 Dec 2022 14:29:14 +0000 Subject: [PATCH] remove memory alloc from statistics_report --- src/tactic/core/elim_uncnstr_tactic.cpp | 3 +-- src/tactic/tactic.h | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp index ed54b67680d..b8b4334f411 100644 --- a/src/tactic/core/elim_uncnstr_tactic.cpp +++ b/src/tactic/core/elim_uncnstr_tactic.cpp @@ -867,8 +867,7 @@ class elim_uncnstr_tactic : public tactic { void run(goal_ref const & g, goal_ref_buffer & result) { bool produce_proofs = g->proofs_enabled(); TRACE("goal", g->display(tout);); - std::function coll = [&](statistics& st) { collect_statistics(st); }; - statistics_report sreport(coll); + statistics_report sreport([&](statistics& st) { collect_statistics(st); }); tactic_report report("elim-uncnstr", *g); m_vars.reset(); collect_occs p; diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h index c43120943dd..ddd18733716 100644 --- a/src/tactic/tactic.h +++ b/src/tactic/tactic.h @@ -120,7 +120,7 @@ class statistics_report { std::function m_collector; public: statistics_report(tactic& t):m_tactic(&t) {} - statistics_report(std::function& coll): m_collector(coll) {} + statistics_report(std::function&& coll): m_collector(std::move(coll)) {} ~statistics_report(); };