From f9ec1f2a637030edcb68bc329f311f9e19f993e8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Nov 2012 09:14:36 -0800 Subject: [PATCH] making sure par-or and par-then combinators work correctly even when OpenMP is not available Signed-off-by: Leonardo de Moura --- src/tactic/tactical.cpp | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index ae9c73a00..d13eab75e 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -545,8 +545,13 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - - if (omp_in_parallel()) { + bool use_seq; +#ifdef _NO_OMP_ + use_seq = true; +#else + use_seq = omp_in_parallel(); +#endif + if (use_seq) { // execute tasks sequentially or_else_tactical::operator()(in, result, mc, pc, core); return; @@ -668,7 +673,13 @@ public: model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { - if (omp_in_parallel()) { + bool use_seq; +#ifdef _NO_OMP_ + use_seq = true; +#else + use_seq = omp_in_parallel(); +#endif + if (use_seq) { // execute tasks sequentially and_then_tactical::operator()(in, result, mc, pc, core); return;