diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index 6bba4663d..460aff29f 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -165,7 +165,6 @@ void fpa2bv_converter::mk_numeral(sort * s, mpf const & v, expr_ref & result) {
         result = m_util.mk_fp(bv_sgn, biased_exp, bv_sig);
         TRACE("fpa2bv_dbg", tout << "value of [" << sign << " " << m_mpz_manager.to_string(sig) << " " << exp << "] is "
             << mk_ismt2_pp(result, m) << std::endl;);
-
     }
 }
 
diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h
index 3f5e76c66..436f44364 100644
--- a/src/ast/fpa/fpa2bv_converter.h
+++ b/src/ast/fpa/fpa2bv_converter.h
@@ -71,9 +71,9 @@ public:
     bool is_rm(expr * e) { return is_app(e) && m_util.is_rm(e); }
     bool is_rm(sort * s) { return m_util.is_rm(s); }
     bool is_float_family(func_decl * f) { return f->get_family_id() == m_util.get_family_id(); }
-    
+
     void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
-    
+
     void split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const;
     void split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const;
 
diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h
index ee7325014..a3215dd6f 100644
--- a/src/ast/fpa_decl_plugin.h
+++ b/src/ast/fpa_decl_plugin.h
@@ -259,7 +259,7 @@ public:
     bool is_rm(sort * s) const { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); }
     bool is_float(expr * e) const { return is_float(m_manager.get_sort(e)); }
     bool is_rm(expr * e) const { return is_rm(m_manager.get_sort(e)); }
-    bool is_fp(expr * e) const { return is_app_of(e, m_fid, OP_FPA_FP); }    
+    bool is_fp(expr * e) const { return is_app_of(e, m_fid, OP_FPA_FP); }
     unsigned get_ebits(sort * s) const;
     unsigned get_sbits(sort * s) const;
 
@@ -294,13 +294,13 @@ public:
     bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pzero(v); }
     bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nzero(v); }
 
-    app * mk_fp(expr * sgn, expr * exp, expr * sig) { 
+    app * mk_fp(expr * sgn, expr * exp, expr * sig) {
         SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1);
         SASSERT(m_bv_util.is_bv(exp));
-        SASSERT(m_bv_util.is_bv(sig));        
-        return m().mk_app(m_fid, OP_FPA_FP, sgn, exp, sig); 
+        SASSERT(m_bv_util.is_bv(sig));
+        return m().mk_app(m_fid, OP_FPA_FP, sgn, exp, sig);
     }
-    
+
     app * mk_to_fp(sort * s, expr * bv_t) {
         SASSERT(is_float(s) && s->get_num_parameters() == 2);
         return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 1, &bv_t);
diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp
index b8d9c232f..92b373ca0 100644
--- a/src/ast/rewriter/fpa_rewriter.cpp
+++ b/src/ast/rewriter/fpa_rewriter.cpp
@@ -98,7 +98,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_FPA_INTERNAL_MIN_UNSPECIFIED:
     case OP_FPA_INTERNAL_MAX_UNSPECIFIED:
         SASSERT(num_args == 2); st = BR_FAILED; break;
-    
+
     case OP_FPA_INTERNAL_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break;
     case OP_FPA_INTERNAL_BV2RM: SASSERT(num_args == 1); st = mk_bv2rm(args[0], result); break;
 
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index ee7559500..fec7922c7 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -116,15 +116,15 @@ namespace smt {
 
         SASSERT(m_trail_stack.get_num_scopes() == 0);
         SASSERT(m_conversions.empty());
-        SASSERT(m_is_added_to_model.empty());        
-    }    
+        SASSERT(m_is_added_to_model.empty());
+    }
     void theory_fpa::init(context * ctx) {
         smt::theory::init(ctx);
         m_is_initialized = true;
     }
 
     app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
-        TRACE("t_fpa_detail", 
+        TRACE("t_fpa_detail",
               ast_manager & m = m_th.get_manager();
               for (unsigned i = 0; i < values.size(); i++)
                   tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
@@ -201,7 +201,7 @@ namespace smt {
     app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
         SASSERT(values.size() == 1);
 
-        TRACE("t_fpa_detail", 
+        TRACE("t_fpa_detail",
               ast_manager & m = m_th.get_manager();
               for (unsigned i = 0; i < values.size(); i++)
               tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
@@ -235,12 +235,12 @@ namespace smt {
         app_ref res(m);
 
         if (m_fpa_util.is_fp(e)) {
-            expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) };            
+            expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) };
             res = m_bv_util.mk_concat(3, cargs);
             m_th_rw((expr_ref&)res);
         }
         else {
-            sort * es = m.get_sort(e);            
+            sort * es = m.get_sort(e);
 
             sort_ref bv_srt(m);
             if (m_converter.is_rm(es))
@@ -264,7 +264,7 @@ namespace smt {
         SASSERT(!m_fpa_util.is_fp(e));
         SASSERT(m_bv_util.is_bv(e));
         SASSERT(m_fpa_util.is_float(s) || m_fpa_util.is_rm(s));
-        ast_manager & m = get_manager();        
+        ast_manager & m = get_manager();
         app_ref res(m);
 
         unsigned bv_sz = m_bv_util.get_bv_size(e);
@@ -285,7 +285,7 @@ namespace smt {
                                    m_bv_util.mk_extract(bv_sz - 2, sbits - 1, e),
                                    m_bv_util.mk_extract(sbits - 2, 0, e));
         }
-        
+
         return res;
     }
 
@@ -312,7 +312,7 @@ namespace smt {
         TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, get_manager()) << std::endl;
                               tout << "converted term: " << mk_ismt2_pp(e_conv, get_manager()) << std::endl;);
 
-        if (m_fpa_util.is_rm(e)) {            
+        if (m_fpa_util.is_rm(e)) {
             SASSERT(m_fpa_util.is_bv2rm(e_conv));
             expr_ref bv_rm(m);
             m_th_rw(to_app(e_conv)->get_arg(0), bv_rm);
@@ -329,7 +329,7 @@ namespace smt {
         }
         else
             UNREACHABLE();
-        
+
         return res;
     }
 
@@ -362,7 +362,7 @@ namespace smt {
                 res = convert_atom(e);
             else if (m_fpa_util.is_float(e) || m_fpa_util.is_rm(e))
                 res = convert_term(e);
-            else 
+            else
                 res = convert_conversion_term(e);
 
             TRACE("t_fpa_detail", tout << "converted; caching:" << std::endl;
@@ -448,7 +448,7 @@ namespace smt {
         TRACE("t_fpa_internalize", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";);
         SASSERT(term->get_family_id() == get_family_id());
         SASSERT(!get_context().e_internalized(term));
-        
+
         ast_manager & m = get_manager();
         context & ctx = get_context();
 
@@ -494,7 +494,7 @@ namespace smt {
         SASSERT(n->get_owner()->get_decl()->get_range() == s);
 
         ast_manager & m = get_manager();
-        context & ctx = get_context();        
+        context & ctx = get_context();
         app_ref owner(n->get_owner(), m);
 
         if (!is_attached_to_var(n)) {
@@ -510,7 +510,7 @@ namespace smt {
                     assert_cnstr(valid);
                 }
             }
-            
+
             if (!ctx.relevancy())
                 relevant_eh(owner);
         }
@@ -600,7 +600,7 @@ namespace smt {
         xe_eq_ye = m.mk_eq(xe, ye);
         not_xe_eq_ye = m.mk_not(xe_eq_ye);
         c_eq_iff = m.mk_iff(not_xe_eq_ye, c);
-        assert_cnstr(c_eq_iff);        
+        assert_cnstr(c_eq_iff);
         assert_cnstr(mk_side_conditions());
 
         return;
@@ -689,10 +689,10 @@ namespace smt {
         pop_scope_eh(m_trail_stack.get_num_scopes());
         m_converter.reset();
         m_rw.reset();
-        m_th_rw.reset();        
-        m_trail_stack.pop_scope(m_trail_stack.get_num_scopes());        
+        m_th_rw.reset();
+        m_trail_stack.pop_scope(m_trail_stack.get_num_scopes());
         if (m_factory) {
-            dealloc(m_factory); 
+            dealloc(m_factory);
             m_factory = 0;
         }
         ast_manager & m = get_manager();
@@ -862,8 +862,8 @@ namespace smt {
     }
 
     bool theory_fpa::include_func_interp(func_decl * f) {
-        TRACE("t_fpa", tout << "f = " << mk_ismt2_pp(f, get_manager()) << std::endl;);        
-        
+        TRACE("t_fpa", tout << "f = " << mk_ismt2_pp(f, get_manager()) << std::endl;);
+
         if (f->get_family_id() == get_family_id()) {
             bool include =
                 m_fpa_util.is_min_unspecified(f) ||
diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp
index 20d8bbbcc..05fedb37f 100644
--- a/src/tactic/fpa/fpa2bv_model_converter.cpp
+++ b/src/tactic/fpa/fpa2bv_model_converter.cpp
@@ -234,7 +234,7 @@ fpa2bv_model_converter::array_model fpa2bv_model_converter::convert_array_func_i
     array_util arr_util(m);
 
     array_model am(m);
-    sort_ref_vector array_domain(m);    
+    sort_ref_vector array_domain(m);
     unsigned arity = f->get_range()->get_num_parameters()-1;
 
     expr_ref as_arr_mdl(m);
@@ -245,21 +245,21 @@ fpa2bv_model_converter::array_model fpa2bv_model_converter::convert_array_func_i
     for (unsigned i = 0; i < arity; i++)
         array_domain.push_back(to_sort(f->get_range()->get_parameter(i).get_ast()));
     sort * rng = to_sort(f->get_range()->get_parameter(arity).get_ast());
-        
+
     bv_f = arr_util.get_as_array_func_decl(to_app(as_arr_mdl));
 
     am.new_float_fd = m.mk_fresh_func_decl(arity, array_domain.c_ptr(), rng);
-    am.new_float_fi = convert_func_interp(am.new_float_fd, bv_f, bv_mdl);    
+    am.new_float_fi = convert_func_interp(am.new_float_fd, bv_f, bv_mdl);
     am.bv_fd = bv_f;
     am.result = arr_util.mk_as_array(f->get_range(), am.new_float_fd);
     return am;
 }
 
-func_interp * fpa2bv_model_converter::convert_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl) {        
+func_interp * fpa2bv_model_converter::convert_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl) {
     SASSERT(f->get_arity() > 0);
     func_interp * result = 0;
     sort * rng = f->get_range();
-    sort * const * dmn = f->get_domain();     
+    sort * const * dmn = f->get_domain();
 
     unsigned arity = bv_f->get_arity();
     func_interp * bv_fi = bv_mdl->get_func_interp(bv_f);
@@ -276,7 +276,7 @@ func_interp * fpa2bv_model_converter::convert_func_interp(func_decl * f, func_de
 
             for (unsigned j = 0; j < arity; j++) {
                 sort * ft_dj = dmn[j];
-                expr * bv_aj = bv_args[j];                
+                expr * bv_aj = bv_args[j];
                 ai = rebuild_floats(bv_mdl, ft_dj, bv_aj);
                 m_th_rw(ai);
                 new_args.push_back(ai);
@@ -293,7 +293,7 @@ func_interp * fpa2bv_model_converter::convert_func_interp(func_decl * f, func_de
         bv_els = bv_fi->get_else();
         ft_els = rebuild_floats(bv_mdl, rng, bv_els);
         m_th_rw(ft_els);
-        result->set_else(ft_els);        
+        result->set_else(ft_els);
     }
 
     return result;
@@ -409,7 +409,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
         it++) {
         seen.insert(it->m_value);
 
-        func_decl * f = it->m_key;        
+        func_decl * f = it->m_key;
         if (f->get_arity() == 0)
         {
             array_util au(m);
@@ -426,7 +426,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
                 bv_mdl->eval(it->m_value, val);
                 if (val) float_mdl->register_decl(f, val);
             }
-        }            
+        }
         else {
             func_interp * fmv = convert_func_interp(f, it->m_value, bv_mdl);
             if (fmv) float_mdl->register_decl(f, fmv);