diff --git a/potassco/basic_types.h b/potassco/basic_types.h
index 73e0be1..e690501 100644
--- a/potassco/basic_types.h
+++ b/potassco/basic_types.h
@@ -178,7 +178,7 @@ class AbstractProgram {
     virtual void project(const AtomSpan& atoms);
     //! Output @c str whenever condition is true in a stable model.
     virtual void output(const std::string_view& str, const LitSpan& condition);
-    //! If @c v is not equal to @c Value_t::release, mark a as external and assume value @c v. Otherwise, treat @c a as
+    //! If `v` is not equal to `Value_t::release`, mark `a` as external and assume value `v`. Otherwise, treat `a` as
     //! regular atom.
     virtual void external(Atom_t a, Value_t v);
     //! Assume the given literals to true during solving.
diff --git a/potassco/platform.h b/potassco/platform.h
index 5edce70..56ada23 100644
--- a/potassco/platform.h
+++ b/potassco/platform.h
@@ -145,6 +145,16 @@ using AbortHandler = void (*)(const char* msg);
  */
 extern AbortHandler setAbortHandler(AbortHandler handler);
 
+//! Sets x87 floating-point unit to double precision if needed and returns the previous configuration.
+/*!
+ * \note This function does nothing (and returns 0) if x87 floating-point unit is not active.
+ * \note x87 floating-point unit is typically only used on x86_32 (x86_64 uses SSE by default).
+ * \return The previous configuration or UINT32_MAX if configuration failed.
+ */
+unsigned initFpuPrecision();
+//! Restores x87 floating-point unit to a previous configuration `r` returned from initFpuPrecision().
+void restoreFpuPrecision(unsigned r);
+
 } // namespace Potassco
 
 ///@}
diff --git a/src/error.cpp b/src/error.cpp
index bea237d..b2c35c4 100644
--- a/src/error.cpp
+++ b/src/error.cpp
@@ -1,16 +1,55 @@
 #include <potassco/error.h>
 
+#if __has_include(<fpu_control.h>)
+#include <fpu_control.h>
+#endif
+
+#include <cfloat>
 #include <charconv>
 #include <cstdarg>
 #include <cstdio>
 #include <span>
 #include <utility>
 
+#if FLT_EVAL_METHOD == 2 || FLT_EVAL_METHOD < 0
+#if defined(_MSC_VER) || defined(_WIN32)
+#pragma fenv_access(on)
+#endif
+static unsigned setFpuPrecision(unsigned* r) {
+#if defined(_FPU_GETCW) && defined(_FPU_SETCW) && defined(_FPU_DOUBLE)
+    fpu_control_t cw;
+    _FPU_GETCW(cw);
+    if (r && cw == static_cast<fpu_control_t>(*r)) {
+        return *r;
+    }
+    auto nw = static_cast<fpu_control_t>(
+        not r ? (cw & ~static_cast<fpu_control_t>(_FPU_EXTENDED) & ~static_cast<fpu_control_t>(_FPU_SINGLE)) |
+                    static_cast<fpu_control_t>(_FPU_DOUBLE)
+              : static_cast<fpu_control_t>(*r));
+    _FPU_SETCW(nw);
+    return static_cast<unsigned>(cw);
+#elif defined(_MSC_VER) || defined(_WIN32)
+    unsigned cw = _controlfp(0, 0);
+    unsigned nw = not r ? static_cast<unsigned>(_PC_53) : *r;
+    _controlfp(nw, _MCW_PC);
+    return cw;
+#else
+    return UINT32_MAX;
+#endif
+    return 0u;
+}
+#else
+constexpr unsigned setFpuPrecision(unsigned*) { return 0u; }
+#endif
+
 namespace Potassco {
 using namespace std::literals;
 
 static constexpr auto c_file = std::string_view{__FILE__};
 
+unsigned initFpuPrecision() { return setFpuPrecision(nullptr); }
+void     restoreFpuPrecision(unsigned r) { setFpuPrecision(&r); }
+
 const char* ExpressionInfo::relativeFileName(const std::source_location& loc) {
     auto res = loc.file_name();
     for (auto cmp = c_file; *res && not cmp.empty() && *res == cmp.front(); cmp.remove_prefix(1), ++res) { ; }