diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
index 4a51e4943..08a29e381 100644
--- a/src/cmd_context/pdecl.cpp
+++ b/src/cmd_context/pdecl.cpp
@@ -189,7 +189,7 @@ class psort_app : public psort {
         m.inc_ref(d);
         m.inc_ref(num_args, args);
         SASSERT(num_args == m_decl->get_num_params() || m_decl->has_var_params());
-        DEBUG_CODE(for (unsigned i = 0; i < num_params; i++) args[i]->check_num_params(this););
+        DEBUG_CODE(if (num_args == num_params) { for (unsigned i = 0; i < num_params; i++) args[i]->check_num_params(this); });
     }
 
     virtual void finalize(pdecl_manager & m) { 
diff --git a/src/duality/duality.h b/src/duality/duality.h
index fc70ffa70..4005adc1a 100755
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -29,7 +29,7 @@ using namespace stl_ext;
 
 namespace Duality {
 
-  class implicant_solver;
+  struct implicant_solver;
 
   /* Generic operations on Z3 formulas */
 
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index ff3bc190b..79055b43a 100755
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -2201,7 +2201,7 @@ namespace Duality {
 #endif
 	    int expand_max = 1;
 	    if(0&&duality->BatchExpand){
-	      int thing = stack.size() * 0.1;
+              int thing = stack.size() / 10; // * 0.1;
 	      expand_max = std::max(1,thing);
 	      if(expand_max > 1)
 		std::cout << "foo!\n";
diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp
index 31af7a53f..c7a8d5aa0 100644
--- a/src/muz/transforms/dl_mk_coi_filter.cpp
+++ b/src/muz/transforms/dl_mk_coi_filter.cpp
@@ -200,7 +200,23 @@ namespace datalog {
             func_decl_set::iterator it = pruned_preds.begin();
             extension_model_converter* mc0 = alloc(extension_model_converter, m);
             for (; it != end; ++it) {
-                mc0->insert(*it, m.mk_true());
+                const rule_vector& rules = source.get_predicate_rules(*it);
+                expr_ref_vector fmls(m);
+                for (unsigned i = 0; i < rules.size(); ++i) {
+                    app* head = rules[i]->get_head();
+                    expr_ref_vector conj(m);
+                    unsigned n = head->get_num_args()-1;
+                    for (unsigned j = 0; j < head->get_num_args(); ++j) {
+                        expr* arg = head->get_arg(j);
+                        if (!is_var(arg)) {
+                            conj.push_back(m.mk_eq(m.mk_var(j, m.get_sort(arg)), arg));
+                        }
+                    }                    
+                    fmls.push_back(m.mk_and(conj.size(), conj.c_ptr()));
+                }
+                expr_ref fml(m);
+                fml = m.mk_or(fmls.size(), fmls.c_ptr());
+                mc0->insert(*it, fml);
             }   
             m_context.add_model_converter(mc0);
         }