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;