diff --git a/src/muz/transforms/dl_mk_bit_blast.cpp b/src/muz/transforms/dl_mk_bit_blast.cpp
index 90d410ab1..15d3b2f5f 100644
--- a/src/muz/transforms/dl_mk_bit_blast.cpp
+++ b/src/muz/transforms/dl_mk_bit_blast.cpp
@@ -71,7 +71,7 @@ namespace datalog {
                 unsigned arity_p = p->get_arity();
                 unsigned arity_q = q->get_arity();
                 SASSERT(0 < arity_p);
-                model->register_decl(p, f);
+                model->register_decl(p, f->copy());
                 func_interp* g = alloc(func_interp, m, arity_q);
 
                 if (f) {
diff --git a/src/tactic/filter_model_converter.cpp b/src/tactic/filter_model_converter.cpp
index da4c71e54..ba6ee4f0d 100644
--- a/src/tactic/filter_model_converter.cpp
+++ b/src/tactic/filter_model_converter.cpp
@@ -43,6 +43,7 @@ void filter_model_converter::operator()(model_ref & old_model, unsigned goal_idx
         if (fs.is_marked(f))
             continue;
         func_interp * fi = old_model->get_func_interp(f);
+        SASSERT(fi);
         new_model->register_decl(f, fi->copy());
     }
     new_model->copy_usort_interps(*old_model);