From 7e8753cd3f50079ae580aa0aa7744cda1de2c6e7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 4 Apr 2020 18:48:09 -0700
Subject: [PATCH] fix #3726

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_solver.cpp                | 1 +
 src/sat/sat_solver/inc_sat_solver.cpp | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index ea827319a..3daf26976 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -3910,6 +3910,7 @@ namespace sat {
             gc_var(lit.var());            
         }
         m_qhead = 0;
+        scoped_suspend_rlimit _sp(m_rlimit);
         propagate(false);
     }
 
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index f82a85c6e..1dcdfbf0a 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -621,7 +621,7 @@ private:
             }
         }
         catch (tactic_exception & ex) {
-            IF_VERBOSE(0, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
+            IF_VERBOSE(1, verbose_stream() << "exception in tactic " << ex.msg() << "\n";);
             set_reason_unknown(ex.msg());
             TRACE("sat", tout << "exception: " << ex.msg() << "\n";);
             m_preprocess = nullptr;