diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp
index cfedb66d7..aa9277e39 100644
--- a/src/tactic/fpa/fpa2bv_tactic.cpp
+++ b/src/tactic/fpa/fpa2bv_tactic.cpp
@@ -93,9 +93,9 @@ class fpa2bv_tactic : public tactic {
                         expr * sgn, *sig, *exp;
                         expr_ref top_exp(m);
                         m_conv.split_fp(new_curr, sgn, exp, sig);
-                        m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1));
-                        m.mk_eq(exp, m_conv.bu().mk_numeral(-1, m_conv.bu().get_bv_size(exp)));
-                        m.mk_eq(sig, m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(sig)));
+                        result.back()->assert_expr(m.mk_eq(sgn, m_conv.bu().mk_numeral(0, 1)));
+                        result.back()->assert_expr(m.mk_eq(exp, m_conv.bu().mk_numeral(-1, m_conv.bu().get_bv_size(exp))));
+                        result.back()->assert_expr(m.mk_eq(sig, m_conv.bu().mk_numeral(1, m_conv.bu().get_bv_size(sig))));
                     }
                 }
             }
@@ -155,7 +155,7 @@ public:
 
     virtual void cleanup() {
         imp * d = alloc(imp, m_imp->m, m_params);
-        std::swap(d, m_imp);        
+        std::swap(d, m_imp);
         dealloc(d);
     }