From f538ee3fe2caf151902b324ce02b8af73c9700b5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 18 May 2020 15:07:39 -0700
Subject: [PATCH] another module level ifdef for #4382

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 6cc6cf6eb..678858fdd 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -19,7 +19,9 @@ Revision History:
 
 
 #include <cmath>
+#ifndef SINGLE_THREAD
 #include <thread>
+#endif
 #include "util/luby.h"
 #include "util/trace.h"
 #include "util/max_cliques.h"
@@ -1322,6 +1324,11 @@ namespace sat {
         return invoke_local_search(num_lits, lits);
     }
 
+#ifdef SINGLE_THREAD
+    lbool solver::check_par(unsigned num_lits, literal const* lits) {
+        return l_undef;
+    }
+#else
     lbool solver::check_par(unsigned num_lits, literal const* lits) {
         if (!rlimit().inc()) {
             return l_undef;
@@ -1468,6 +1475,7 @@ namespace sat {
         return result;
 
     }
+#endif
 
     /*
       \brief import lemmas/units from parallel sat solvers.