From 54a8d656179fc092cc62bf9652700e06821cc429 Mon Sep 17 00:00:00 2001 From: yizhou7 Date: Fri, 2 Dec 2022 16:56:53 -0500 Subject: [PATCH] move flushes in display_statistics (#6472) --- src/shell/smtlib_frontend.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index d0d0b452d..220001b40 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/src/shell/smtlib_frontend.cpp @@ -44,12 +44,12 @@ static void display_statistics() { lock_guard lock(*display_stats_mux); clock_t end_time = clock(); if (g_cmd_context && g_display_statistics) { - std::cout.flush(); - std::cerr.flush(); if (g_cmd_context) { g_cmd_context->set_regular_stream("stdout"); g_cmd_context->display_statistics(true, ((static_cast(end_time) - static_cast(g_start_time)) / CLOCKS_PER_SEC)); } + std::cout.flush(); + std::cerr.flush(); } }