--- 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");