diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index c456da29b..ab13e751a 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -2809,6 +2809,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
 
         expr * e = m.mk_eq(m_util.mk_to_real(result), x);
         m_extra_assertions.push_back(e);
+        // x = 0 -> result = 0+
+        m_extra_assertions.push_back(m.mk_implies(m.mk_eq(x, zero), m.mk_eq(result, m_util.mk_pzero(result->get_sort()))));
     }
 
     SASSERT(is_well_sorted(m, result));
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 01282a53b..c5b897d78 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1653,7 +1653,7 @@ public:
                 return FC_CONTINUE;
             }
             for (expr* e : m_not_handled) {
-                if (!ctx().is_relevant(e) && false)
+                if (!ctx().is_relevant(e))
                     continue;
                 st = FC_DONE;
                 switch (eval_unsupported(e)) {