diff --git a/ir/type.cpp b/ir/type.cpp
index 404fae097..b4e6accf4 100644
--- a/ir/type.cpp
+++ b/ir/type.cpp
@@ -6,6 +6,7 @@
 #include "ir/state.h"
 #include "smt/solver.h"
 #include "util/compiler.h"
+#include "util/config.h"
 #include <array>
 #include <cassert>
 #include <numeric>
@@ -450,7 +451,7 @@ expr FloatType::fromFloat(State &s, const expr &fp, const Type &from_type0,
   expr isnan = fp.isNaN();
   expr val = fp.float2BV();
 
-  if (isnan.isFalse())
+  if (config::use_exact_fp || isnan.isFalse())
     return val;
 
   unsigned fraction_bits = fractionBits();
diff --git a/util/config.cpp b/util/config.cpp
index 82ab5f66a..dd11aac72 100644
--- a/util/config.cpp
+++ b/util/config.cpp
@@ -15,6 +15,7 @@ bool skip_smt = false;
 string smt_benchmark_dir;
 bool disable_poison_input = false;
 bool disable_undef_input = false;
+bool use_exact_fp = false;
 bool tgt_is_asm = false;
 bool fail_if_src_is_ub = false;
 bool disallow_ub_exploitation = false;
diff --git a/util/config.h b/util/config.h
index 57f58c888..397168875 100644
--- a/util/config.h
+++ b/util/config.h
@@ -19,6 +19,8 @@ extern bool disable_poison_input;
 
 extern bool disable_undef_input;
 
+extern bool use_exact_fp;
+
 extern bool tgt_is_asm;
 
 extern bool fail_if_src_is_ub;