diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp
index 8ebb3375d..e82c06386 100644
--- a/src/tactic/fpa/fpa2bv_model_converter.cpp
+++ b/src/tactic/fpa/fpa2bv_model_converter.cpp
@@ -38,7 +38,7 @@ void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) {
     m_bv2fp->convert_rm_consts(mc, float_mdl, seen);
     m_bv2fp->convert_min_max_specials(mc, float_mdl, seen);
     m_bv2fp->convert_uf2bvuf(mc, float_mdl, seen);
-    
+
     // Keep all the non-float constants.
     unsigned sz = mc->get_num_constants();
     for (unsigned i = 0; i < sz; i++) {
@@ -46,7 +46,7 @@ void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) {
         if (!seen.contains(c))
             float_mdl->register_decl(c, mc->get_const_interp(c));
     }
-    
+
     // And keep everything else
     sz = mc->get_num_functions();
     for (unsigned i = 0; i < sz; i++) {
@@ -57,7 +57,7 @@ void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) {
             float_mdl->register_decl(f, val);
         }
     }
-    
+
     sz = mc->get_num_uninterpreted_sorts();
     for (unsigned i = 0; i < sz; i++) {
         sort * s = mc->get_uninterpreted_sort(i);
diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h
index 465aaa1e4..989caaa58 100644
--- a/src/tactic/fpa/fpa2bv_model_converter.h
+++ b/src/tactic/fpa/fpa2bv_model_converter.h
@@ -26,7 +26,7 @@ Notes:
 class fpa2bv_model_converter : public model_converter {
     ast_manager & m;
     bv2fpa_converter * m_bv2fp;
-    
+
 public:
     fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & conv):
         m(m),
@@ -53,10 +53,10 @@ public:
     virtual model_converter * translate(ast_translation & translator);
 
 protected:
-    fpa2bv_model_converter(ast_manager & m) : 
+    fpa2bv_model_converter(ast_manager & m) :
         m(m),
         m_bv2fp(0) {}
-    
+
     void convert(model_core * mc, model * float_mdl);
 };