From acb9376ea03a240ebad7a82601db3c2fb90dc53f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 23 Mar 2020 10:57:15 -0700
Subject: [PATCH] fix #3488

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

diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index bbb163fee..90deecbd1 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1327,6 +1327,9 @@ namespace sat {
     }
 
     lbool solver::check_par(unsigned num_lits, literal const* lits) {
+        if (!rlimit().inc()) {
+            return l_undef;
+        }
         scoped_ptr_vector<i_local_search> ls;
         scoped_ptr_vector<solver> uw;
         int num_extra_solvers = m_config.m_num_threads - 1;
@@ -1442,6 +1445,11 @@ namespace sat {
             }
         };
 
+        if (!rlimit().inc()) {
+            set_par(nullptr, 0);
+            return l_undef;
+        }
+
         vector<std::thread> threads(num_threads);
         for (int i = 0; i < num_threads; ++i) {
             threads[i] = std::thread([&, i]() { worker_thread(i); });