diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp
index d24f506a1..bbbc00783 100644
--- a/src/tactic/bv/bv_size_reduction_tactic.cpp
+++ b/src/tactic/bv/bv_size_reduction_tactic.cpp
@@ -25,6 +25,7 @@ Notes:
 #include"bv_decl_plugin.h"
 #include"expr_replacer.h"
 #include"extension_model_converter.h"
+#include"filter_model_converter.h"
 #include"ast_smt2_pp.h"
 
 class bv_size_reduction_tactic : public tactic {
@@ -60,6 +61,7 @@ struct bv_size_reduction_tactic::imp {
     obj_map<app, numeral>     m_unsigned_lowers;
     obj_map<app, numeral>     m_unsigned_uppers;
     ref<bv_size_reduction_mc> m_mc;
+    ref<filter_model_converter> m_fmc;
     scoped_ptr<expr_replacer> m_replacer;
     bool                      m_produce_models;
     volatile bool             m_cancel;
@@ -196,6 +198,7 @@ struct bv_size_reduction_tactic::imp {
                         numeral u = m_util.norm(entry->get_data().m_value, bv_sz, true);
                         TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << "\n";);
                         expr * new_def = 0;
+                        app  * new_const = 0;
                         if (l > u) {
                             g.assert_expr(m.mk_false());
                             return;
@@ -208,15 +211,19 @@ struct bv_size_reduction_tactic::imp {
                             if (l.is_neg()) {
                                 unsigned i_nb = (u - l).get_num_bits();
                                 unsigned v_nb = m_util.get_bv_size(v);
-                                if (i_nb < v_nb)
-                                    new_def = m_util.mk_sign_extend(v_nb - i_nb, m.mk_fresh_const(0, m_util.mk_sort(i_nb)));
+                                if (i_nb < v_nb) {
+                                    new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb));
+                                    new_def = m_util.mk_sign_extend(v_nb - i_nb, new_const);
+                                }
                             }
                             else {
                                 // 0 <= l <= v <= u
                                 unsigned u_nb = u.get_num_bits();
                                 unsigned v_nb = m_util.get_bv_size(v);
-                                if (u_nb < v_nb)
-                                    new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), m.mk_fresh_const(0, m_util.mk_sort(u_nb)));
+                                if (u_nb < v_nb) {
+                                    new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb));
+                                    new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);
+                                }
                             }
                         }
                     
@@ -226,6 +233,10 @@ struct bv_size_reduction_tactic::imp {
                                 if (!m_mc) 
                                     m_mc = alloc(bv_size_reduction_mc, m);
                                 m_mc->insert(v->get_decl(), new_def);
+                                if (!m_fmc && new_const) 
+                                    m_fmc = alloc(filter_model_converter, m);
+                                if (new_const) 
+                                    m_fmc->insert(new_const->get_decl());
                             }
                             num_reduced++;
                         }
@@ -264,6 +275,7 @@ struct bv_size_reduction_tactic::imp {
 
                     TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << "\n";);
                     expr * new_def = 0;
+                    app * new_const = 0;
                     if (l > u) {
                         g.assert_expr(m.mk_false());
                         return;
@@ -275,8 +287,10 @@ struct bv_size_reduction_tactic::imp {
                         // 0 <= l <= v <= u
                         unsigned u_nb = u.get_num_bits();
                         unsigned v_nb = m_util.get_bv_size(v);
-                        if (u_nb < v_nb)
-                            new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), m.mk_fresh_const(0, m_util.mk_sort(u_nb)));
+                        if (u_nb < v_nb) {
+                            new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);
+                            new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb));
+                        }
                     }
                     
                     if (new_def) {
@@ -285,6 +299,10 @@ struct bv_size_reduction_tactic::imp {
                             if (!m_mc) 
                                 m_mc = alloc(bv_size_reduction_mc, m);
                             m_mc->insert(v->get_decl(), new_def);
+                            if (!m_fmc && new_const) 
+                                m_fmc = alloc(filter_model_converter, m);
+                            if (new_const) 
+                                m_fmc->insert(new_const->get_decl());
                         }
                         num_reduced++;
                         TRACE("bv_size_reduction", tout << "New definition = " << mk_ismt2_pp(new_def, m) << "\n";);
@@ -309,7 +327,11 @@ struct bv_size_reduction_tactic::imp {
                 g.update(i, new_f);
             }
             mc   = m_mc.get();
+            if (m_fmc) {
+                mc = concat(m_fmc.get(), mc.get());
+            }
             m_mc = 0;
+            m_fmc = 0;
         }
         report_tactic_progress(":bv-reduced", num_reduced);
         TRACE("after_bv_size_reduction", g.display(tout); if (m_mc) m_mc->display(tout););