diff --git a/src/ast/ast.h b/src/ast/ast.h
index 475e58ac7..f71d5135c 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -667,6 +667,8 @@ public:
     expr * get_arg(unsigned idx) const { SASSERT(idx < m_num_args); return m_args[idx]; }
     expr * const * get_args() const { return m_args; }
     unsigned get_size() const { return get_obj_size(get_num_args()); }
+    expr * const * begin() const { return m_args; }
+    expr * const * end() const { return m_args + m_num_args; }
 
     unsigned get_depth() const { return flags()->m_depth; }
     bool is_ground() const { return flags()->m_ground; }
diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp
index cac6f1f5d..3ae72215f 100644
--- a/src/tactic/bv/dt2bv_tactic.cpp
+++ b/src/tactic/bv/dt2bv_tactic.cpp
@@ -30,6 +30,7 @@ Revision History:
 #include "var_subst.h"
 #include "ast_util.h"
 #include "enum2bv_rewriter.h"
+#include "ast_pp.h"
 
 
 class dt2bv_tactic : public tactic {
@@ -53,36 +54,38 @@ class dt2bv_tactic : public tactic {
 
         void operator()(app* a) {
             if (m.is_eq(a)) {
-                return;
+                // no-op
             }
-            if (m.is_distinct(a)) {
-                return;
+            else if (m.is_distinct(a)) {
+                // no-op
             }
-            if (m_t.m_dt.is_recognizer(a->get_decl()) &&
+            else if (m_t.m_dt.is_recognizer(a->get_decl()) &&
                 m_t.is_fd(a->get_arg(0))) {
                 m_t.m_fd_sorts.insert(get_sort(a->get_arg(0)));
-                return;
             }
-
-            if (m_t.is_fd(a) && a->get_num_args() > 0) {
+            else if (m_t.is_fd(a) && a->get_num_args() > 0) {
                 m_t.m_non_fd_sorts.insert(get_sort(a));
+                args_cannot_be_fd(a);
             }
             else if (m_t.is_fd(a)) {
                 m_t.m_fd_sorts.insert(get_sort(a));
             }
             else {
-                unsigned sz = a->get_num_args();
-                for (unsigned i = 0; i < sz; ++i) {
-                    if (m_t.is_fd(a->get_arg(i))) {
-                        m_t.m_non_fd_sorts.insert(get_sort(a->get_arg(i)));
-                    }
-                }
+                args_cannot_be_fd(a);
+            }
+        }
+
+        void args_cannot_be_fd(app* a) {
+            for (expr* arg : *a) {
+                if (m_t.is_fd(arg)) {
+                    m_t.m_non_fd_sorts.insert(get_sort(arg));
+                }                    
             }
         }
 
         void operator()(var * v) {
             if (m_t.is_fd(v)) {
-                m_t.m_non_fd_sorts.insert(get_sort(v));
+                m_t.m_fd_sorts.insert(get_sort(v));
             }
         }