From 7df8d176392335dbb791d454695c76e58bd3c833 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 1 Feb 2020 10:59:48 -0800
Subject: [PATCH] move in assumptions to loop

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

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 746b53771..d0dcf6e50 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3449,14 +3449,15 @@ namespace smt {
         if (!check_preamble(reset_cancel)) return l_undef;
         SASSERT(at_base_level());
         setup_context(false);
-        expr_ref_vector asms(m, num_assumptions, assumptions);
         if (m_fparams.m_threads > 1) {            
+            expr_ref_vector asms(m, num_assumptions, assumptions);
             parallel p(*this);
             return p(asms);
         }
         lbool r;
         do {
             pop_to_base_lvl();
+            expr_ref_vector asms(m, num_assumptions, assumptions);
             internalize_assertions();
             add_theory_assumptions(asms);                
             TRACE("unsat_core_bug", tout << asms << "\n";);