From cb4ceeab3ac10c10f6e681e6cb79b9bdf48d785c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 16 Apr 2020 12:04:46 -0700
Subject: [PATCH] fix #3985

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index dcabeacbd..848ee02da 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1492,8 +1492,8 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     if (m_ignore_check)
         return;
     IF_VERBOSE(100, verbose_stream() << "(started \"check-sat\")" << std::endl;);
-    TRACE("before_check_sat", dump_assertions(tout););
     init_manager();
+    TRACE("before_check_sat", dump_assertions(tout););
     unsigned timeout = m_params.m_timeout;
     unsigned rlimit  = m_params.rlimit();
     scoped_watch sw(*this);
@@ -1613,10 +1613,6 @@ void cmd_context::get_consequences(expr_ref_vector const& assumptions, expr_ref_
 
 
 void cmd_context::reset_assertions() {
-    if (!m_global_decls) {
-        reset(false);
-        return;
-    }
 
     if (m_opt) {
         m_opt = nullptr;