From 918b6a8c038532d272a1c9aef9835883ce17cd4b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Apr 2020 13:58:22 -0700 Subject: [PATCH] trace & threads = undef Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 2 +- src/solver/parallel_tactic.cpp | 2 ++ src/tactic/tactical.cpp | 6 ++++++ 3 files changed, 9 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 80285536d..aaf9d3406 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3466,7 +3466,7 @@ namespace smt { SASSERT(!m_setup.already_configured()); setup_context(m_fparams.m_auto_config); - if (m_fparams.m_threads > 1) { + if (m_fparams.m_threads > 1 && !m.has_trace_stream()) { parallel p(*this); expr_ref_vector asms(m); return p(asms); diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index b6f7cd231..71a99ea79 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -715,6 +715,8 @@ public: cleanup(); fail_if_proof_generation("parallel-tactic", g); ast_manager& m = g->m(); + if (m.has_trace_stream()) + throw default_exception("parallel tactic does not work with trace"); solver* s = m_solver->translate(m, m_params); solver_state* st = alloc(solver_state, nullptr, s, m_params); m_queue.add_task(st); diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index ba4e7e661..2f902fbb2 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -391,6 +391,9 @@ public: ast_manager & m = in->m(); + if (m.has_trace_stream()) + throw default_exception("threads and trace are incompatible"); + scoped_ptr_vector managers; scoped_limits scl(m.limit()); goal_ref_vector in_copies; @@ -662,6 +665,9 @@ public: } }; + if (m.has_trace_stream()) + throw default_exception("threads and trace are incompatible"); + vector threads(r1_size); for (unsigned i = 0; i < r1_size; ++i) { threads[i] = std::thread([&, i]() { worker_thread(i); });