diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index c2e58a9e7..f19fae369 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -211,7 +211,7 @@ namespace datalog {
         m_var_subst(m),
         m_rule_manager(*this),
         m_contains_p(*this),
-        m_check_pred(m_contains_p, m),
+        m_rule_properties(m, m_rule_manager, *this, m_contains_p),
         m_transf(*this),
         m_trail(*this),
         m_pinned(m),
@@ -452,10 +452,7 @@ namespace datalog {
             rm.mk_rule(fml, p, m_rule_set, m_rule_names[m_rule_fmls_head]);
             ++m_rule_fmls_head;
         }
-        rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
-        for (; it != end; ++it) {
-            check_rule(*(*it));
-        }
+        check_rules(m_rule_set);
     }
 
     //
@@ -541,140 +538,49 @@ namespace datalog {
         m_engine->add_cover(level, pred, property);
     }
 
-    void context::check_uninterpreted_free(rule& r) {
-        func_decl* f = 0;
-        if (get_rule_manager().has_uninterpreted_non_predicates(r, f)) {
-            std::stringstream stm;
-            stm << "Uninterpreted '" 
-                << f->get_name() 
-                << "' in ";
-            r.display(*this, stm);
-            throw default_exception(stm.str());
-        }
-    }
-
-    void context::check_quantifier_free(rule& r) {
-        if (get_rule_manager().has_quantifiers(r)) {
-            std::stringstream stm;
-            stm << "cannot process quantifiers in rule ";
-            r.display(*this, stm);
-            throw default_exception(stm.str());
-        }
-    }
-
-
-    void context::check_existential_tail(rule& r) {
-        unsigned ut_size = r.get_uninterpreted_tail_size();
-        unsigned t_size  = r.get_tail_size();   
-        
-        TRACE("dl", get_rule_manager().display_smt2(r, tout); tout << "\n";);
-        for (unsigned i = ut_size; i < t_size; ++i) {
-            app* t = r.get_tail(i);
-            TRACE("dl", tout << "checking: " << mk_ismt2_pp(t, get_manager()) << "\n";);
-            if (m_check_pred(t)) {
-                std::ostringstream out;
-                out << "interpreted body " << mk_ismt2_pp(t, get_manager()) << " contains recursive predicate";
-                throw default_exception(out.str());
-            }
-        }
-    }
-
-    void context::check_positive_predicates(rule& r) {
-        ast_mark visited;
-        ptr_vector<expr> todo, tocheck;
-        unsigned ut_size = r.get_uninterpreted_tail_size();
-        unsigned t_size  = r.get_tail_size();   
-        for (unsigned i = 0; i < ut_size; ++i) {
-            if (r.is_neg_tail(i)) {
-                tocheck.push_back(r.get_tail(i));
-            }
-        }
-        ast_manager& m = get_manager();
-        contains_pred contains_p(*this);
-        check_pred check_pred(contains_p, get_manager());
-
-        for (unsigned i = ut_size; i < t_size; ++i) {
-            todo.push_back(r.get_tail(i));
-        }
-        while (!todo.empty()) {
-            expr* e = todo.back(), *e1, *e2;
-            todo.pop_back();
-            if (visited.is_marked(e)) {
-                continue;
-            }
-            visited.mark(e, true);
-            if (is_predicate(e)) {
-            }
-            else if (m.is_and(e) || m.is_or(e)) {
-                todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
-            }
-            else if (m.is_implies(e, e1, e2)) {
-                tocheck.push_back(e1);
-                todo.push_back(e2);
-            }
-            else if (is_quantifier(e)) {
-                todo.push_back(to_quantifier(e)->get_expr());
-            }
-            else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) && 
-                     m.is_true(e1)) {
-                todo.push_back(e2);
-            }
-            else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) &&
-                     m.is_true(e2)) {
-                todo.push_back(e1);
-            }
-            else {
-                tocheck.push_back(e);
-            }
-        }
-        for (unsigned i = 0; i < tocheck.size(); ++i) {
-            expr* e = tocheck[i];
-            if (check_pred(e)) {
-                std::ostringstream out;
-                out << "recursive predicate " << mk_ismt2_pp(e, get_manager()) << " occurs nested in body";
-                r.display(*this, out << "\n");
-                throw default_exception(out.str());
-
-            }
-        }
-    }
-
-#if 0
     void context::check_rules(rule_set& r) {
+        m_rule_properties.set_generate_proof(generate_proof_trace());
         switch(get_engine()) {
-        case DATALOG_ENGINE:
-            collect_properties(r);
-            check_quantifier_free(r);
-            check_uninterpreted_free(r);
-            check_existential_tail(r); 
+        case DATALOG_ENGINE:            
+            m_rule_properties.collect(r);
+            m_rule_properties.check_quantifier_free();
+            m_rule_properties.check_uninterpreted_free();
+            m_rule_properties.check_nested_free(); 
             break;
         case PDR_ENGINE:
-            check_existential_tail(r);
-            check_positive_predicates(r);
-            check_uninterpreted_free(r);
+            m_rule_properties.collect(r);
+            m_rule_properties.check_existential_tail();
+            m_rule_properties.check_for_negated_predicates();
+            m_rule_properties.check_uninterpreted_free();
             break;
         case QPDR_ENGINE:
-            check_positive_predicates(r);
-            check_uninterpreted_free(r);
+            m_rule_properties.collect(r);
+            m_rule_properties.check_for_negated_predicates();
+            m_rule_properties.check_uninterpreted_free();
             break;
         case BMC_ENGINE:
-            check_positive_predicates(r);
+            m_rule_properties.collect(r);
+            m_rule_properties.check_for_negated_predicates();
             break;            
         case QBMC_ENGINE:
-            check_existential_tail(r);
-            check_positive_predicates(r);
+            m_rule_properties.collect(r);
+            m_rule_properties.check_existential_tail();
+            m_rule_properties.check_for_negated_predicates();
             break;         
         case TAB_ENGINE:
-            check_existential_tail(r);
-            check_positive_predicates(r);
+            m_rule_properties.collect(r);
+            m_rule_properties.check_existential_tail();
+            m_rule_properties.check_for_negated_predicates();
             break;
 	case DUALITY_ENGINE:
-            check_existential_tail(r);
-            check_positive_predicates(r);
+            m_rule_properties.collect(r);
+            m_rule_properties.check_existential_tail();
+            m_rule_properties.check_for_negated_predicates();
             break;
         case CLP_ENGINE:
-            check_existential_tail(r);
-            check_positive_predicates(r);
+            m_rule_properties.collect(r);
+            m_rule_properties.check_existential_tail();
+            m_rule_properties.check_for_negated_predicates();
             break;
         case DDNF_ENGINE:
             break;
@@ -683,57 +589,6 @@ namespace datalog {
             UNREACHABLE();
             break;
         }
-        if (generate_proof_trace() && !r.get_proof()) {
-            m_rule_manager.mk_rule_asserted_proof(r);
-        }
-    }
-#endif
-
-    void context::check_rule(rule& r) {
-        switch(get_engine()) {
-        case DATALOG_ENGINE:
-            check_quantifier_free(r);
-            check_uninterpreted_free(r);
-            check_existential_tail(r); 
-            break;
-        case PDR_ENGINE:
-            check_existential_tail(r);
-            check_positive_predicates(r);
-            check_uninterpreted_free(r);
-            break;
-        case QPDR_ENGINE:
-            check_positive_predicates(r);
-            check_uninterpreted_free(r);
-            break;
-        case BMC_ENGINE:
-            check_positive_predicates(r);
-            break;            
-        case QBMC_ENGINE:
-            check_existential_tail(r);
-            check_positive_predicates(r);
-            break;         
-        case TAB_ENGINE:
-            check_existential_tail(r);
-            check_positive_predicates(r);
-            break;
-	case DUALITY_ENGINE:
-            check_existential_tail(r);
-            check_positive_predicates(r);
-            break;
-        case CLP_ENGINE:
-            check_existential_tail(r);
-            check_positive_predicates(r);
-            break;
-        case DDNF_ENGINE:
-            break;
-        case LAST_ENGINE:
-        default:
-            UNREACHABLE();
-            break;
-        }
-        if (generate_proof_trace() && !r.get_proof()) {
-            m_rule_manager.mk_rule_asserted_proof(r);
-        }
     }
 
     void context::add_rule(rule_ref& r) {
@@ -984,11 +839,7 @@ namespace datalog {
         // TODO: what?
         if(get_engine() != DUALITY_ENGINE) {
           new_query();
-	  rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
-	  rule_ref r(m_rule_manager);
-	  for (; it != end; ++it) {
-            check_rule(*(*it));
-	  }     
+          check_rules(m_rule_set);	       
         }   
 #endif
         m_mc = mk_skip_model_converter();
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index e96752721..285726026 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -42,6 +42,7 @@ Revision History:
 #include"expr_functors.h"
 #include"dl_engine_base.h"
 #include"bind_variables.h"
+#include"rule_properties.h"
 
 struct fixedpoint_params;
 
@@ -141,6 +142,17 @@ namespace datalog {
             SK_UINT64,
             SK_SYMBOL
         };
+        class contains_pred : public i_expr_pred {
+            context const& ctx;
+        public:
+            contains_pred(context& ctx): ctx(ctx) {}
+            virtual ~contains_pred() {}
+            
+            virtual bool operator()(expr* e) {
+                return ctx.is_predicate(e);
+            }
+        };
+
 
     private:
         class sort_domain;
@@ -154,17 +166,6 @@ namespace datalog {
         typedef obj_map<const func_decl, svector<symbol> > pred2syms;
         typedef obj_map<const sort, sort_domain*> sort_domain_map;
 
-        class contains_pred : public i_expr_pred {
-            context const& ctx;
-        public:
-            contains_pred(context& ctx): ctx(ctx) {}
-            virtual ~contains_pred() {}
-            
-            virtual bool operator()(expr* e) {
-                return ctx.is_predicate(e);
-            }
-        };
-
 
         ast_manager &      m;
         register_engine_base& m_register_engine;
@@ -179,7 +180,7 @@ namespace datalog {
         var_subst          m_var_subst;
         rule_manager       m_rule_manager;
         contains_pred      m_contains_p;
-        check_pred         m_check_pred;
+        rule_properties    m_rule_properties;
         rule_transformer   m_transf;
         trail_stack<context> m_trail;
         ast_ref_vector     m_pinned;
@@ -419,7 +420,7 @@ namespace datalog {
         /**
           \brief Check if rule is well-formed according to engine.
         */
-        void check_rule(rule& r);
+        void check_rules(rule_set& r);
 
         /**
            \brief Return true if facts to \c pred can be added using the \c add_table_fact() function.
@@ -565,11 +566,6 @@ namespace datalog {
 
         void ensure_engine();
 
-        void check_quantifier_free(rule& r);        
-        void check_uninterpreted_free(rule& r);
-        void check_existential_tail(rule& r);
-        void check_positive_predicates(rule& r);
-
         // auxilary functions for SMT2 pretty-printer.
         void declare_vars(expr_ref_vector& rules, mk_fresh_name& mk_fresh, std::ostream& out);
 
diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp
new file mode 100644
index 000000000..7f019c74e
--- /dev/null
+++ b/src/muz/base/rule_properties.cpp
@@ -0,0 +1,189 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    rule_properties.cpp
+
+Abstract:
+
+    Collect properties of rules.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 9-25-2014
+
+Notes:
+    
+
+--*/
+
+#include"expr_functors.h"
+#include"rule_properties.h"
+#include"dl_rule_set.h"
+#include"for_each_expr.h"
+#include"dl_context.h"
+
+using namespace datalog;
+rule_properties::rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& p): 
+    m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_generate_proof(false) {}
+
+rule_properties::~rule_properties() {}
+
+void rule_properties::collect(rule_set const& rules) {
+    reset();
+    rule_set::iterator it = rules.begin(), end = rules.end();
+    expr_sparse_mark visited;
+    for (; it != end; ++it) {
+        rule* r = *it;
+        m_rule = r;
+        unsigned ut_size = r->get_uninterpreted_tail_size();
+        unsigned t_size  = r->get_tail_size();  
+        if (r->has_negation()) {
+            m_negative_rules.push_back(r);            
+        }
+        for (unsigned i = ut_size; i < t_size; ++i) {
+            for_each_expr_core<rule_properties,expr_sparse_mark, true, false>(*this, visited, r->get_tail(i));
+        }
+        if (m_generate_proof && !r->get_proof()) {
+            rm.mk_rule_asserted_proof(*r);
+        }
+    }     
+}
+
+void rule_properties::check_quantifier_free() {
+    if (!m_quantifiers.empty()) {
+        quantifier* q = m_quantifiers.begin()->m_key;
+        rule* r = m_quantifiers.begin()->m_value;
+        std::stringstream stm;
+        stm << "cannot process quantifier in rule ";
+        r->display(m_ctx, stm);
+        throw default_exception(stm.str());
+    }
+}
+
+void rule_properties::check_for_negated_predicates() {
+    if (!m_negative_rules.empty()) {
+        rule* r = m_negative_rules[0];
+        std::stringstream stm;
+        stm << "Rule contains negative predicate ";
+        r->display(m_ctx, stm);
+        throw default_exception(stm.str());        
+    }
+}
+
+
+void rule_properties::check_uninterpreted_free() {    
+    if (!m_uninterp_funs.empty()) {
+        func_decl* f = m_uninterp_funs.begin()->m_key;
+        rule* r = m_uninterp_funs.begin()->m_value;
+        std::stringstream stm;
+        stm << "Uninterpreted '" 
+            << f->get_name() 
+            << "' in ";
+        r->display(m_ctx, stm);
+        throw default_exception(stm.str());
+    }
+}
+
+void rule_properties::check_nested_free() {
+    if (!m_interp_pred.empty()) {
+        std::stringstream stm;
+        rule* r = m_interp_pred[0];
+        stm << "Rule contains nested predicates ";
+        r->display(m_ctx, stm);
+        throw default_exception(stm.str());
+
+    }
+}
+
+void rule_properties::check_existential_tail() {
+    ast_mark visited;
+    ptr_vector<expr> todo, tocheck;
+    for (unsigned i = 0; i < m_interp_pred.size(); ++i) {
+        rule& r = *m_interp_pred[i];
+        unsigned ut_size = r.get_uninterpreted_tail_size();
+        unsigned t_size  = r.get_tail_size();   
+        for (unsigned i = ut_size; i < t_size; ++i) {
+            todo.push_back(r.get_tail(i));
+        }
+    }
+    context::contains_pred contains_p(m_ctx);
+    check_pred check_pred(contains_p, m);
+    
+    while (!todo.empty()) {
+        expr* e = todo.back(), *e1, *e2;
+        todo.pop_back();
+        if (visited.is_marked(e)) {
+            continue;
+        }
+        visited.mark(e, true);
+        if (m_is_predicate(e)) {
+        }
+        else if (m.is_and(e) || m.is_or(e)) {
+            todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
+        }
+        else if (m.is_implies(e, e1, e2)) {
+            tocheck.push_back(e1);
+            todo.push_back(e2);
+        }
+        else if (is_quantifier(e)) {
+            todo.push_back(to_quantifier(e)->get_expr());
+        }
+        else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) && 
+                 m.is_true(e1)) {
+            todo.push_back(e2);
+        }
+        else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) &&
+                 m.is_true(e2)) {
+            todo.push_back(e1);
+        }
+        else {
+            tocheck.push_back(e);
+        }
+    }
+    for (unsigned i = 0; i < tocheck.size(); ++i) {
+        expr* e = tocheck[i];
+        if (check_pred(e)) {
+            std::ostringstream out;
+            out << "recursive predicate " << mk_ismt2_pp(e, m) << " occurs nested in the body of a rule";
+            throw default_exception(out.str());            
+        }
+    }
+}
+
+
+void rule_properties::insert(ptr_vector<rule>& rules, rule* r) {
+    if (rules.empty() || rules.back() != r) {
+        rules.push_back(r);
+    }
+}
+
+void rule_properties::operator()(var* n) { }
+
+void rule_properties::operator()(quantifier* n) {
+    m_quantifiers.insert(n, m_rule);
+}
+void rule_properties::operator()(app* n) {
+    if (m_is_predicate(n)) {
+        insert(m_interp_pred, m_rule);
+    }    
+    else if (is_uninterp(n)) {
+        m_uninterp_funs.insert(n->get_decl(), m_rule);
+    }
+    else if (m_dt.is_accessor(n)) {
+        sort* s = m.get_sort(n->get_arg(0));
+        SASSERT(m_dt.is_datatype(s));
+        if (m_dt.get_datatype_constructors(s)->size() > 1) {
+            m_uninterp_funs.insert(n->get_decl(), m_rule);
+        }
+    }
+}
+
+void rule_properties::reset() {
+    m_quantifiers.reset();
+    m_uninterp_funs.reset();
+    m_interp_pred.reset();
+    m_negative_rules.reset();
+}
+
diff --git a/src/muz/base/rule_properties.h b/src/muz/base/rule_properties.h
new file mode 100644
index 000000000..bfff8cbe4
--- /dev/null
+++ b/src/muz/base/rule_properties.h
@@ -0,0 +1,60 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    rule_properties.h
+
+Abstract:
+
+    Collect properties of rules.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 9-25-2014
+
+Notes:
+    
+
+--*/
+
+#ifndef _RULE_PROPERTIES_H_
+#define _RULE_PROPERTIES_H_
+
+#include"ast.h"
+#include"datatype_decl_plugin.h"
+#include"dl_rule.h"
+
+namespace datalog {
+    class rule_properties {
+        ast_manager&  m;
+        rule_manager& rm;
+        context&      m_ctx;
+        i_expr_pred&  m_is_predicate;
+        datatype_util m_dt;
+        bool          m_generate_proof;
+        rule*         m_rule;
+        obj_map<quantifier, rule*> m_quantifiers;
+        obj_map<func_decl, rule*>  m_uninterp_funs;
+        ptr_vector<rule>           m_interp_pred;
+        ptr_vector<rule>           m_negative_rules;
+
+        void insert(ptr_vector<rule>& rules, rule* r);
+    public:
+        rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& is_predicate);
+        ~rule_properties();    
+        void set_generate_proof(bool generate_proof) { m_generate_proof = generate_proof; } 
+        void collect(rule_set const& r);
+        void check_quantifier_free();
+        void check_uninterpreted_free();
+        void check_existential_tail();
+        void check_for_negated_predicates();
+        void check_nested_free();
+        void operator()(var* n);
+        void operator()(quantifier* n);
+        void operator()(app* n);
+        void reset();
+    };
+}
+
+#endif /* _RULE_PROPERTIES_H_ */
diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp
index bb991c65f..4aba180f6 100644
--- a/src/test/dl_query.cpp
+++ b/src/test/dl_query.cpp
@@ -143,8 +143,11 @@ void dl_query_test_wpa(smt_params & fparams, params_ref& params) {
     ctx.updt_params(params);
     {
         wpa_parser* p = wpa_parser::create(ctx, m);
-        TRUSTME( p->parse_directory(problem_dir) );
+        bool = ok = p->parse_directory(problem_dir);
         dealloc(p);
+        if (!ok) {
+            std::cout << "Could not parse: " << problem_dir << "\n";
+        }
     }
 
     const unsigned attempts = 10;