diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp
index 676ba0c69..cfd022124 100644
--- a/src/api/z3_replayer.cpp
+++ b/src/api/z3_replayer.cpp
@@ -225,6 +225,13 @@ struct z3_replayer::imp {
         return curr() == '-' || curr() == '.' || ('0' <= curr() && curr() <= '9') || curr() == 'e' || curr() == 'E'; 
     }
 
+#if (!defined(strtof))
+    float strtof(const char * str, char ** end_ptr) {
+        // Note: This may introduce a double-rounding problem.
+        return (float)strtod(str, end_ptr);
+    }
+#endif
+
     void read_float() {
         m_string.reset();
         while (is_double_char()) {
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index d51e34058..d6d1420e3 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -146,7 +146,6 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
         app_ref bv(m);
         unsigned bv_sz = 1 + ebits + (sbits - 1);
         bv = mk_fresh_const(0, bv_sz);
-        m_fresh_bv_variables.insert(bv);
 
         sgn = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv);
         e = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv);