From 89ff533dcdb449a7f8e95006c165abaf20dcea52 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 17 Mar 2020 11:08:30 -0700
Subject: [PATCH] port fix #3376 from Debug branch

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_parallel.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp
index 131e7504b..edfb4d120 100644
--- a/src/smt/smt_parallel.cpp
+++ b/src/smt/smt_parallel.cpp
@@ -50,6 +50,7 @@ namespace smt {
         scoped_ptr_vector<context> pctxs;
         vector<expr_ref_vector> pasms;
         ast_manager& m = ctx.m;
+        scoped_limits sl(m.limit());
         unsigned finished_id = UINT_MAX;
         std::string        ex_msg;
         par_exception_kind ex_kind = DEFAULT_EX;
@@ -66,6 +67,7 @@ namespace smt {
             new_ctx.set_random_seed(i + ctx.get_fparams().m_random_seed);
             ast_translation tr(m, *new_m);
             pasms.push_back(tr(asms));
+            sl.push_child(&(new_m->limit()));
         }
 
         auto cube = [](context& ctx, expr_ref_vector& lasms, expr_ref& c) {