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

ensure parallel mode works under push/pop

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-04 19:22:28 -08:00
parent 69ca840ceb
commit 3da3b41786
4 changed files with 16 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/smt/smt_context.cpp
View file

@ -155,15 +155,16 @@ namespace smt {
return std::min(m_relevancy_lvl, m_fparams.m_relevancy_lvl);
}
void context::copy(context& src_ctx, context& dst_ctx) {
void context::copy(context& src_ctx, context& dst_ctx, bool override_base) {
ast_manager& dst_m = dst_ctx.get_manager();
ast_manager& src_m = src_ctx.get_manager();
src_ctx.pop_to_base_lvl();
if (src_ctx.m_base_lvl > 0) {
if (!override_base && src_ctx.m_base_lvl > 0) {
INVOKE_DEBUGGER();
throw default_exception("Cloning contexts within a user-scope is not allowed");
}
SASSERT(src_ctx.m_base_lvl == 0);
SASSERT(src_ctx.m_base_lvl == 0 || override_base);
ast_translation tr(src_m, dst_m, false);