diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp
index 59e9e6fec..930bd5483 100644
--- a/src/muz_qe/horn_tactic.cpp
+++ b/src/muz_qe/horn_tactic.cpp
@@ -90,21 +90,30 @@ class horn_tactic : public tactic {
             m_ctx.register_predicate(to_app(a)->get_decl(), true);
         }
 
-        void check_predicate(expr* a) {
-            expr* a1 = 0;
-            while (true) {
+        void check_predicate(ast_mark& mark, expr* a) {
+            ptr_vector<expr> todo;
+            todo.push_back(a);
+            while (!todo.empty()) {
+                a = todo.back();
+                todo.pop_back();
+                if (mark.is_marked(a)) {
+                    continue;
+                }
+                mark.mark(a, true);
                 if (is_quantifier(a)) {
                     a = to_quantifier(a)->get_expr();
-                    continue;
+                    todo.push_back(a);
                 }
-                if (m.is_not(a, a1)) {
-                    a = a1;
-                    continue;
+                else if (m.is_not(a) || m.is_and(a) || m.is_or(a) || m.is_implies(a)) {
+                    todo.append(to_app(a)->get_num_args(), to_app(a)->get_args());
                 }
-                if (is_predicate(a)) {
+                else if (m.is_ite(a)) {
+                    todo.append(to_app(a)->get_arg(1));
+                    todo.append(to_app(a)->get_arg(2));
+                }
+                else if (is_predicate(a)) {
                     register_predicate(a);
                 }
-                break;
             }
         }
 
@@ -112,14 +121,15 @@ class horn_tactic : public tactic {
 
         formula_kind get_formula_kind(expr_ref& f) {
             normalize(f);
+            ast_mark mark;
             expr_ref_vector args(m), body(m);
             expr_ref head(m);
             expr* a = 0, *a1 = 0;
             datalog::flatten_or(f, args);
             for (unsigned i = 0; i < args.size(); ++i) {
-                a = args[i].get();    
-                check_predicate(a);
-                if (m.is_not(a, a1) && is_predicate(a1)) {
+                a = args[i].get(); 
+                check_predicate(mark, a);
+                if (m.is_not(a, a1)) {
                     body.push_back(a1);
                 }
                 else if (is_predicate(a)) {
@@ -128,9 +138,6 @@ class horn_tactic : public tactic {
                     }
                     head = a;
                 }
-                else if (m.is_not(a, a1)) {
-                    body.push_back(a1);
-                }
                 else {
                     body.push_back(m.mk_not(a));
                 }
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 2f43d518c..e56c332a1 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -1827,10 +1827,8 @@ namespace pdr {
             proof_ref pr(m);
             pr = m.mk_asserted(m.mk_true());
             for (unsigned i = 0; i < vars.size(); ++i) {    
-                if (smt::is_value_sort(m, vars[i].get())) {
-                    tmp = mev.eval(M, vars[i].get());
-                    sub.insert(vars[i].get(), tmp, pr);
-                }
+                tmp = mev.eval(M, vars[i].get());
+                sub.insert(vars[i].get(), tmp, pr);
             }
             if (!rep) rep = mk_expr_simp_replacer(m);
             rep->set_substitution(&sub);
diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp
index 8a36e9089..db11b5b20 100644
--- a/src/muz_qe/pdr_util.cpp
+++ b/src/muz_qe/pdr_util.cpp
@@ -608,6 +608,7 @@ namespace pdr {
        best effort evaluator of extensional array equality.
      */
     void model_evaluator::eval_array_eq(app* e, expr* arg1, expr* arg2) {
+        TRACE("pdr", tout << "array equality: " << mk_pp(e, m) << "\n";);
         expr_ref v1(m), v2(m);
         m_model->eval(arg1, v1);
         m_model->eval(arg2, v2);
@@ -633,7 +634,10 @@ namespace pdr {
 
         if (else1 != else2) {
             if (m.is_value(else1) && m.is_value(else2)) {
-                set_bool(e, false);
+                TRACE("pdr", tout 
+                      << "defaults are different: " << mk_pp(e, m) << " " 
+                      << mk_pp(else1, m) << " " << mk_pp(else2, m) << "\n";);
+                set_false(e);
             }
             else {
                 TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";);
@@ -659,7 +663,10 @@ namespace pdr {
                 continue;
             }
             else if (m.is_value(w1) && m.is_value(w2)) {
-                set_bool(e, false);
+                TRACE("pdr", tout << "Equality evaluation: " << mk_pp(e, m) << "\n"; 
+                      tout << mk_pp(s1, m) << " |-> " << mk_pp(w1, m) << "\n";
+                      tout << mk_pp(s2, m) << " |-> " << mk_pp(w2, m) << "\n";);
+                set_false(e);
                 return;
             }
             else {
@@ -668,7 +675,7 @@ namespace pdr {
                 return;
             }
         }
-        set_bool(e, true);                
+        set_true(e);
     }
 
     void model_evaluator::eval_eq(app* e, expr* arg1, expr* arg2) {
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index f0c491f64..9f2c97a84 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -102,6 +102,7 @@ template<typename Ext>
 bool theory_diff_logic<Ext>::internalize_term(app * term) {
     bool result = null_theory_var != mk_term(term);
     CTRACE("arith", !result, tout << "Did not internalize " << mk_pp(term, get_manager()) << "\n";);
+    TRACE("non_diff_logic", tout << "Terms may not be internalized\n";);
     found_non_diff_logic_expr(term);
     return result;
 }
@@ -831,6 +832,7 @@ theory_var theory_diff_logic<Ext>::mk_var(app* n) {
         v = mk_var(e);
     }      
     if (is_interpreted(n)) {
+        TRACE("non_diff_logic", tout << "Variable should not be interpreted\n";);
         found_non_diff_logic_expr(n);
     }
     TRACE("arith", tout << mk_pp(n, get_manager()) << " |-> " << v << "\n";);