diff --git a/src/sat/bsat2/System.h b/src/sat/bsat2/System.h
index e3d8afba2..f5ed5fa13 100644
--- a/src/sat/bsat2/System.h
+++ b/src/sat/bsat2/System.h
@@ -22,7 +22,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #define Minisat_System_h
 
 #if defined(__linux__)
-#include <fpu_control.h>
+//#include <fpu_control.h>
 #endif
 
 #include "sat/bsat2/IntTypes.h"
@@ -39,26 +39,35 @@ extern double memUsedPeak();        // Peak-memory in mega bytes (returns 0 for
 
 }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 //-------------------------------------------------------------------------------------------------
 // Implementation of inline functions:
 
 #if defined(_MSC_VER) || defined(__MINGW32__)
 #include <time.h>
 
+ABC_NAMESPACE_CXX_HEADER_START
+
 static inline double Minisat::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; }
 
+ABC_NAMESPACE_CXX_HEADER_END
+
 #else
 #include <sys/time.h>
 #include <sys/resource.h>
 #include <unistd.h>
 
+ABC_NAMESPACE_CXX_HEADER_START
+
 static inline double Minisat::cpuTime(void) {
     struct rusage ru;
     getrusage(RUSAGE_SELF, &ru);
     return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; }
 
-#endif
-
 ABC_NAMESPACE_CXX_HEADER_END
 
 #endif
+
+
+#endif