diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index d649ac236..67704719b 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -101,40 +101,31 @@ struct evaluator_cfg : public default_rewriter_cfg {
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
         result_pr = 0;
         family_id fid = f->get_family_id();
-        if (fid == null_family_id) {
-            if (num == 0) {
-                expr * val = m_model.get_const_interp(f);
-                if (val != 0) {
-                    result = val;
-                    return BR_DONE;
-                }
-                
-                if (m_model_completion) {
-                    sort * s   = f->get_range();
-                    expr * val = m_model.get_some_value(s);
-                    m_model.register_decl(f, val);
-                    result = val;
-                    return BR_DONE;
-                }
-                return BR_FAILED;
-            }
-            SASSERT(num > 0);
-            func_interp * fi = m_model.get_func_interp(f);
-            if (fi != 0 && eval_fi(fi, num, args, result)) {
-                TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n";
-                      for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
-                      tout << "---->\n" << mk_ismt2_pp(result, m()) << "\n";);
+        if (fid == null_family_id && num == 0) {
+            expr * val = m_model.get_const_interp(f);
+            if (val != 0) {
+                result = val;
                 return BR_DONE;
             }
+            
+            if (m_model_completion) {
+                sort * s   = f->get_range();
+                expr * val = m_model.get_some_value(s);
+                m_model.register_decl(f, val);
+                result = val;
+                return BR_DONE;
+            }
+            return BR_FAILED;
         }
 
+        br_status st = BR_FAILED;
+
         if (fid == m_b_rw.get_fid()) {
             decl_kind k = f->get_decl_kind();
             if (k == OP_EQ) {
                 // theory dispatch for =
                 SASSERT(num == 2);
                 family_id s_fid = m().get_sort(args[0])->get_family_id();
-                br_status st = BR_FAILED;
                 if (s_fid == m_a_rw.get_fid())
                     st = m_a_rw.mk_eq_core(args[0], args[1], result);
                 else if (s_fid == m_bv_rw.get_fid())
@@ -148,54 +139,70 @@ struct evaluator_cfg : public default_rewriter_cfg {
             }
             return m_b_rw.mk_app_core(f, num, args, result);
         }
+
         if (fid == m_a_rw.get_fid())
-            return m_a_rw.mk_app_core(f, num, args, result);
-        if (fid == m_bv_rw.get_fid())
-            return m_bv_rw.mk_app_core(f, num, args, result);
-        if (fid == m_ar_rw.get_fid()) 
-            return m_ar_rw.mk_app_core(f, num, args, result);
-        if (fid == m_dt_rw.get_fid())
-            return m_dt_rw.mk_app_core(f, num, args, result);
-        if (fid == m_pb_rw.get_fid())
-            return m_pb_rw.mk_app_core(f, num, args, result);
-        if (fid == m_f_rw.get_fid())
-            return m_f_rw.mk_app_core(f, num, args, result);
-        return BR_FAILED;
+            st = m_a_rw.mk_app_core(f, num, args, result);
+        else if (fid == m_bv_rw.get_fid())
+            st = m_bv_rw.mk_app_core(f, num, args, result);
+        else if (fid == m_ar_rw.get_fid()) 
+            st = m_ar_rw.mk_app_core(f, num, args, result);
+        else if (fid == m_dt_rw.get_fid())
+            st = m_dt_rw.mk_app_core(f, num, args, result);
+        else if (fid == m_pb_rw.get_fid())
+            st = m_pb_rw.mk_app_core(f, num, args, result);
+        else if (fid == m_f_rw.get_fid())
+            st = m_f_rw.mk_app_core(f, num, args, result);
+
+        // allow for model evaluation to work on result of rewriting.
+        if (st == BR_DONE && is_app(result) && to_app(result)->get_num_args() > 0) {
+            return BR_REWRITE1;
+        }
+
+        if (st == BR_FAILED) {
+            func_interp * fi = m_model.get_func_interp(f);
+            if (fi != 0 && eval_fi(fi, num, args, result)) {
+                TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n";
+                      for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
+                      tout << "---->\n" << mk_ismt2_pp(result, m()) << "\n";);
+                return BR_DONE;
+            }
+            TRACE("model_evaluator", tout << f->get_name() << "\n";);
+        }
+
+        return st;
     }
 
     bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) { 
-        if (f->get_family_id() == null_family_id) {
-            func_interp * fi = m_model.get_func_interp(f);
-            
-            if (fi != 0) {
-                if (fi->is_partial()) {
-                    if (m_model_completion) {
-                        sort * s   = f->get_range();
-                        expr * val = m_model.get_some_value(s);
-                        fi->set_else(val);
-                    }
-                    else {
-                        return false;
-                    }
+
+        func_interp * fi = m_model.get_func_interp(f);        
+        if (fi != 0) {
+            if (fi->is_partial()) {
+                if (m_model_completion) {
+                    sort * s   = f->get_range();
+                    expr * val = m_model.get_some_value(s);
+                    fi->set_else(val);
                 }
-                
-                def    = fi->get_interp();
-                SASSERT(def != 0);
-                return true;
-            }
-            
-            if (m_model_completion) {
-                sort * s   = f->get_range();
-                expr * val = m_model.get_some_value(s);
-                func_interp * new_fi = alloc(func_interp, m(), f->get_arity());
-                new_fi->set_else(val);
-                m_model.register_decl(f, new_fi);
-                def = val;
-                return true;
-            }
+                else {
+                    return false;
+                }
+            }            
+            def    = fi->get_interp();
+            SASSERT(def != 0);
+            return true;
+        }
+
+        if (f->get_family_id() == null_family_id && m_model_completion) {
+            sort * s   = f->get_range();
+            expr * val = m_model.get_some_value(s);
+            func_interp * new_fi = alloc(func_interp, m(), f->get_arity());
+            new_fi->set_else(val);
+            m_model.register_decl(f, new_fi);
+            def = val;
+            return true;
         }
         return false;
     }
+
     
     bool max_steps_exceeded(unsigned num_steps) const { 
         cooperate("model evaluator");
diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp
index 6c138fd57..98d982b7a 100644
--- a/src/smt/smt_model_generator.cpp
+++ b/src/smt/smt_model_generator.cpp
@@ -400,7 +400,12 @@ namespace smt {
        \brief Return true if the interpretation of the function should be included in the model.
     */
     bool model_generator::include_func_interp(func_decl * f) const {
-        return f->get_family_id() == null_family_id;
+        family_id fid = f->get_family_id();
+        if (fid == null_family_id) return true;
+        if (fid == m_manager.get_basic_family_id()) return false;
+        theory * th   = m_context->get_theory(fid);
+        if (!th) return true;
+        return th->include_func_interp(f);
     }
     
     /**
diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h
index 242ad7c17..c5fb80a1e 100644
--- a/src/smt/smt_theory.h
+++ b/src/smt/smt_theory.h
@@ -412,6 +412,10 @@ namespace smt {
             return 0;
         }
 
+        virtual bool include_func_interp(func_decl* f) {
+            return false;
+        }
+
         // -----------------------------------
         //
         // Model checker
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 0622f03ff..581fbb4df 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1346,7 +1346,7 @@ namespace smt {
                 empty_column ||
                 (unbounded_gain(max_gain) == (x_i == null_theory_var)));
         
-        return !empty_column && safe_gain(min_gain, max_gain);
+        return safe_gain(min_gain, max_gain);
     }
 
     template<typename Ext>
@@ -1557,14 +1557,12 @@ namespace smt {
                     // variable cannot be used for max/min.
                     continue; 
                 }
-                bool picked_var = pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, 
+                bool safe_to_leave = pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, 
                                                     curr_min_gain, curr_max_gain, 
                                                     has_shared, curr_x_i);
 
-
-                SASSERT(!picked_var || safe_gain(curr_min_gain, curr_max_gain));
                 
-                if (!safe_gain(curr_min_gain, curr_max_gain)) {
+                if (!safe_to_leave) {
                     TRACE("opt", tout << "no variable picked\n";);
                     has_bound = true;
                     best_efforts++;
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 6bcae6f60..dcf06e1e5 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1283,6 +1283,21 @@ namespace smt {
         theory::reset_eh();
     }
 
+    bool theory_bv::include_func_interp(func_decl* f) {
+        SASSERT(f->get_family_id() == get_family_id());
+        switch (f->get_decl_kind()) {
+        case OP_BSDIV0:
+        case OP_BUDIV0:
+        case OP_BSREM0:
+        case OP_BUREM0:       
+        case OP_BSMOD0:        
+            return true;
+        default:
+            return false;
+        }
+        return false;
+    }
+
     theory_bv::theory_bv(ast_manager & m, theory_bv_params const & params, bit_blaster_params const & bb_params):
         theory(m.mk_family_id("bv")),
         m_params(params),
diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h
index 0f74b3603..414474a89 100644
--- a/src/smt/theory_bv.h
+++ b/src/smt/theory_bv.h
@@ -236,6 +236,7 @@ namespace smt {
         virtual void pop_scope_eh(unsigned num_scopes);
         virtual final_check_status final_check_eh();
         virtual void reset_eh();
+        virtual bool include_func_interp(func_decl* f);
         svector<theory_var>   m_merge_aux[2]; //!< auxiliary vector used in merge_zero_one_bits
         bool merge_zero_one_bits(theory_var r1, theory_var r2);