mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

ensure smt2log works with multi-threaded consumers, ease scenarios around #5655

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-11-19 11:02:50 -08:00
parent 5194aa186a
commit ca2c2bb802
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/api/api_solver.cpp
View file

@ -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());
}
}