diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp
index 04f50a53e..0e5145f66 100644
--- a/src/muz/base/dl_rule_set.cpp
+++ b/src/muz/base/dl_rule_set.cpp
@@ -394,19 +394,18 @@ namespace datalog {
     */
     bool rule_set::stratified_negation() {
         ptr_vector<rule>::const_iterator it  = m_rules.c_ptr();
-        ptr_vector<rule>::const_iterator end = m_rules.c_ptr()+m_rules.size();
+        ptr_vector<rule>::const_iterator end = m_rules.c_ptr() + m_rules.size();
         for (; it != end; it++) {
             rule * r = *it;
-            app * head = r->get_head();
-            func_decl * head_decl = head->get_decl();
+            func_decl * head_decl = r->get_decl();
             unsigned n = r->get_uninterpreted_tail_size();
             for (unsigned i = r->get_positive_tail_size(); i < n; i++) {
                 SASSERT(r->is_neg_tail(i));
-                func_decl * tail_decl = r->get_tail(i)->get_decl();
+                func_decl * tail_decl = r->get_decl(i);
                 unsigned neg_strat = get_predicate_strat(tail_decl);
                 unsigned head_strat = get_predicate_strat(head_decl);
 
-                SASSERT(head_strat>=neg_strat); //head strat can never be lower than that of a tail
+                SASSERT(head_strat >= neg_strat); // head strat can never be lower than that of a tail
                 if (head_strat == neg_strat) {
                     return false;
                 }
diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index b8485a1f7..b15171e88 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -358,6 +358,8 @@ class horn_tactic : public tactic {
                 not_supported("xform.instantiate_arrays");
             if (p.xform_magic())
                 not_supported("xform.magic");
+            if (p.xform_quantify_arrays())
+                not_supported("xform.quantify_arrays");
         }
 
         void not_supported(char const* s) {