diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 659e4c4a4d1..207bf030a65 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -158,10 +158,19 @@ extern "C" { init_solver_core(c, s); } + static std::thread::id g_thread_id = std::this_thread::get_id(); + static bool g_is_threaded = false; + static void init_solver_log(Z3_context c, Z3_solver s) { solver_params sp(to_solver(s)->m_params); symbol smt2log = sp.smtlib2_log(); if (smt2log.is_non_empty_string() && !to_solver(s)->m_pp) { + if (g_is_threaded || g_thread_id != std::this_thread::get_id()) { + g_is_threaded = true; + std::ostringstream strm; + strm << smt2log << "-" << std::this_thread::get_id(); + smt2log = symbol(strm.str()); + } to_solver(s)->m_pp = alloc(solver2smt2_pp, mk_c(c)->m(), smt2log.str()); } }