diff --git a/src/muz/dataflow/dataflow.h b/src/muz/dataflow/dataflow.h
index 9e100121a..1e52c5f93 100644
--- a/src/muz/dataflow/dataflow.h
+++ b/src/muz/dataflow/dataflow.h
@@ -87,6 +87,7 @@ namespace datalog {
             for (func_decl_set::iterator I = output_preds.begin(),
                 E = output_preds.end(); I != E; ++I) {
                 func_decl* sym = *I;
+                TRACE("dl", tout << sym->get_name() << "\n";);
                 const rule_vector& output_rules = m_rules.get_predicate_rules(sym);
                 for (unsigned i = 0; i < output_rules.size(); ++i) {
                     m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value.init_down(m_context, output_rules[i]);
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index d349da4ec..4cdc76ede 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -738,6 +738,7 @@ namespace pdr {
     // model_node
 
     void model_node::set_closed() {
+        TRACE("pdr", tout << state() << "\n";);
         pt().close(state());
         m_closed = true; 
     }
@@ -928,7 +929,7 @@ namespace pdr {
         model_node* p = n.parent();
         while (p) {
             if (p->state() == n.state()) {
-                TRACE("pdr", tout << "repeated\n";);
+                TRACE("pdr", tout << n.state() << "repeated\n";);
                 return true;
             }
             p = p->parent();
@@ -1018,6 +1019,11 @@ namespace pdr {
             SASSERT(n1->children().empty());
             enqueue_leaf(n1);
         }
+
+        if (!nodes.empty() && n.get_model_ptr() && backtrack) {
+            model_ref mr(n.get_model_ptr());
+            nodes[0]->set_model(mr);
+        }
         if (nodes.empty()) {            
             cache(n).remove(n.state());
         }
@@ -1149,17 +1155,21 @@ namespace pdr {
             ast_manager& m = n->pt().get_manager();
             if (!n->get_model_ptr()) {
                 if (models.find(n->state(), md)) {
-                    TRACE("pdr", tout << mk_pp(n->state(), m) << "\n";);
+                    TRACE("pdr", tout << n->state() << "\n";);
                     model_ref mr(md);
                     n->set_model(mr);
                     datalog::rule const* rule = rules.find(n->state());
                     n->set_rule(rule);
                 }
                 else {
+                    TRACE("pdr", tout << "no model for " << n->state() << "\n";);
                     IF_VERBOSE(1, n->display(verbose_stream() << "no model:\n", 0);
-                               verbose_stream() << mk_pp(n->state(), m) << "\n";);
+                               verbose_stream() << n->state() << "\n";);
                 }
             }
+            else {
+                TRACE("pdr", tout << n->state() << "\n";);
+            }
             todo.pop_back();
             todo.append(n->children().size(), n->children().c_ptr());
         }        
@@ -2027,11 +2037,11 @@ namespace pdr {
             switch (expand_state(n, cube, uses_level)) {
             case l_true:
                 if (n.level() == 0) {
-                    TRACE("pdr", tout << "reachable at level 0\n";);
+                    TRACE("pdr", n.display(tout << "reachable at level 0\n", 0););
                     close_node(n);
                 }
                 else {
-                    TRACE("pdr", tout << "node: " << &n << "\n";); 
+                    TRACE("pdr", n.display(tout, 0);); 
                     create_children(n);
                 }
                 break;
diff --git a/src/muz/pdr/pdr_context.h b/src/muz/pdr/pdr_context.h
index 7cba1e0c5..35b9067b2 100644
--- a/src/muz/pdr/pdr_context.h
+++ b/src/muz/pdr/pdr_context.h
@@ -240,7 +240,7 @@ namespace pdr {
         void check_pre_closed();
         void set_closed();     
         void set_open();
-        void set_pre_closed() { m_closed = true; }
+        void set_pre_closed() { TRACE("pdr", tout << state() << "\n";); m_closed = true; }
         void reset() { m_children.reset(); }
 
         void set_rule(datalog::rule const* r) { m_rule = r; }
diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp
index 67b88724c..c452e2611 100644
--- a/src/muz/transforms/dl_mk_coi_filter.cpp
+++ b/src/muz/transforms/dl_mk_coi_filter.cpp
@@ -41,6 +41,9 @@ namespace datalog {
             bool new_tail = false;
             bool contained = true;
             for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) {
+                if (m_context.has_facts(r->get_decl(i))) {
+                    return 0;
+                }
                 if (r->is_neg_tail(i)) {
                     if (!engine.get_fact(r->get_decl(i)).is_reachable()) {
                         if (!new_tail) {
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 2d3a60ea8..1bb521923 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -154,7 +154,7 @@ namespace opt {
         m_soft_constraints(m), m_answer(m) {}
 
     lbool maxsmt::operator()() {
-        lbool is_sat;
+        lbool is_sat = l_undef;
         m_msolver = 0;
         symbol const& maxsat_engine = m_c.maxsat_engine();
         IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);