--- simp/Main.cc.orig	2010-07-10 10:07:36.000000000 -0600
+++ simp/Main.cc	2011-06-22 15:13:36.468390581 -0600
@@ -74,7 +74,7 @@ int main(int argc, char** argv)
         setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n  where input may be either in plain or gzipped DIMACS.\n");
         // printf("This is MiniSat 2.0 beta\n");
         
-#if defined(__linux__)
+#if defined(__linux__) && defined(_FPU_EXTENDED) && defined(_FPU_DOUBLE)
         fpu_control_t oldcw, newcw;
         _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
         printf("WARNING: for repeatability, setting FPU to use double precision\n");