diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index 59ab65bbd..ecd9ee5cb 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -1608,12 +1608,14 @@ namespace datalog {
         expr* const* axioms = m_background.c_ptr();
         expr_ref fml(m);
         expr_ref_vector rules(m);
+        svector<symbol> names;
         bool use_fixedpoint_extensions = m_params.get_bool(":print-with-fixedpoint-extensions", true);
         {
             rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
             for (; it != end; ++it) {
                 (*it)->to_formula(fml);
                 rules.push_back(fml);
+                names.push_back((*it)->name());
             }
         }
 
@@ -1680,11 +1682,18 @@ namespace datalog {
         }
         for (unsigned i = 0; i < rules.size(); ++i) {            
             out << (use_fixedpoint_extensions?"(rule ":"(assert ");
+            expr* r = rules[i].get();
+            if (symbol::null != names[i]) {
+                out << "(! ";
+            }
             if (use_fixedpoint_extensions) {
-                ast_smt2_pp(out, rules[i].get(), env, params);
+                ast_smt2_pp(out, r, env, params);
             }
             else {
-                out << mk_smt_pp(rules[i].get(), m);
+                out << mk_smt_pp(r, m);
+            }
+            if (symbol::null != names[i]) {
+                out << " :named " << names[i] << ")";
             }
             out << ")\n";
         }
diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp
index 33298c515..f4d8fd557 100644
--- a/src/muz_qe/pdr_util.cpp
+++ b/src/muz_qe/pdr_util.cpp
@@ -466,6 +466,7 @@ void model_evaluator::eval_arith(app* e) {
 }
 
 void model_evaluator::inherit_value(expr* e, expr* v) {
+    expr* w;
     SASSERT(!is_unknown(v));
     SASSERT(m.get_sort(e) == m.get_sort(v));
     if (is_x(v)) {
@@ -475,7 +476,10 @@ void model_evaluator::inherit_value(expr* e, expr* v) {
         SASSERT(m.is_bool(v));
         if (is_true(v)) set_true(e);
         else if (is_false(v)) set_false(e);
-        else set_x(e);
+        else {
+            TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";);
+            set_x(e);
+        }
     }
     else if (m_arith.is_int_real(e)) {
         set_number(e, get_number(v));
@@ -483,7 +487,11 @@ void model_evaluator::inherit_value(expr* e, expr* v) {
     else if (m.is_value(v)) {
         set_value(e, v);
     }
+    else if (m_values.find(v, w)) {
+        set_value(e, w);
+    }
     else {
+        TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";);
         set_x(e);
     }
 }
@@ -642,6 +650,7 @@ void model_evaluator::eval_basic(app* e) {
                 set_bool(e, e1 == e2);
             }
             else {
+                TRACE("pdr", tout << "not value equal:\n" << mk_pp(e1, m) << "\n" << mk_pp(e2, m) << "\n";);
                 set_x(e);
             }
         }
diff --git a/src/muz_qe/proof_utils.cpp b/src/muz_qe/proof_utils.cpp
index 6143e6746..75c9cbb15 100644
--- a/src/muz_qe/proof_utils.cpp
+++ b/src/muz_qe/proof_utils.cpp
@@ -223,7 +223,7 @@ public:
                     found_false = true;
                     break;
                 }
-                SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
+                // SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
                 parents.push_back(tmp);          
                 if (is_closed(tmp) && !m_units.contains(m.get_fact(tmp))) {
                     m_units.insert(m.get_fact(tmp), tmp);
@@ -283,7 +283,7 @@ public:
                     found_false = true;
                     break;
                 }
-                SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
+                // SASSERT(m.get_fact(tmp) == m.get_fact(m.get_parent(p, i)));
                 change = change || (tmp != m.get_parent(p, i));
                 args.push_back(tmp);
             }