From 35a3523fd6fb612fc796f6c0d1794ea1e5a93373 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 11 Dec 2017 14:09:34 -0800
Subject: [PATCH] fix bug in double collection of declarations

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.h              |  3 +++
 src/ast/decl_collector.cpp | 25 ++++++++++---------------
 src/ast/decl_collector.h   |  2 +-
 3 files changed, 14 insertions(+), 16 deletions(-)

diff --git a/src/ast/ast.h b/src/ast/ast.h
index e579e4565..682660638 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -622,6 +622,9 @@ public:
     sort * const * get_domain() const { return m_domain; }
     sort * get_range() const { return m_range; }
     unsigned get_size() const { return get_obj_size(m_arity); }
+    sort * const * begin() const { return get_domain(); }
+    sort * const * end() const { return get_domain() + get_arity(); }
+
 };
 
 // -----------------------------------
diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp
index 0df4b0fc5..5d47170ee 100644
--- a/src/ast/decl_collector.cpp
+++ b/src/ast/decl_collector.cpp
@@ -20,20 +20,15 @@ Revision History:
 #include "ast/decl_collector.h"
 
 void decl_collector::visit_sort(sort * n) {
+    SASSERT(!m_visited.is_marked(n));
     family_id fid = n->get_family_id();
     if (m().is_uninterp(n))
         m_sorts.push_back(n);
-    if (fid == m_dt_fid) {
+    else if (fid == m_dt_fid) {
         m_sorts.push_back(n);
-
-        unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(n);
-        for (unsigned i = 0; i < num_cnstr; i++) {
-            func_decl * cnstr = m_dt_util.get_datatype_constructors(n)->get(i);
+        for (func_decl* cnstr : *m_dt_util.get_datatype_constructors(n)) {
             m_decls.push_back(cnstr);
-            ptr_vector<func_decl> const & cnstr_acc = *m_dt_util.get_constructor_accessors(cnstr);
-            unsigned num_cas = cnstr_acc.size();
-            for (unsigned j = 0; j < num_cas; j++) {
-                func_decl * accsr = cnstr_acc.get(j);
+            for (func_decl * accsr : *m_dt_util.get_constructor_accessors(cnstr)) {
                 m_decls.push_back(accsr);
             }
         }
@@ -53,6 +48,7 @@ void decl_collector::visit_func(func_decl * n) {
             else
                 m_decls.push_back(n);
         }
+        m_visited.mark(n, true);
     }
 }
 
@@ -72,11 +68,10 @@ void decl_collector::visit(ast* n) {
         if (!m_visited.is_marked(n)) {
             switch(n->get_kind()) {
             case AST_APP: {
-                app * a = to_app(n);
-                for (unsigned i = 0; i < a->get_num_args(); ++i) {
-                    m_todo.push_back(a->get_arg(i));
+                for (expr * e : *to_app(n)) {
+                    m_todo.push_back(e);
                 }
-                m_todo.push_back(a->get_decl());
+                m_todo.push_back(to_app(n)->get_decl());
                 break;
             }
             case AST_QUANTIFIER: {
@@ -96,8 +91,8 @@ void decl_collector::visit(ast* n) {
                 break;
             case AST_FUNC_DECL: {
                 func_decl * d = to_func_decl(n);
-                for (unsigned i = 0; i < d->get_arity(); ++i) {
-                    m_todo.push_back(d->get_domain(i));
+                for (sort* srt : *d) {
+                    m_todo.push_back(srt);
                 }
                 m_todo.push_back(d->get_range());
                 visit_func(d);
diff --git a/src/ast/decl_collector.h b/src/ast/decl_collector.h
index 0a812bb2c..36d7c930b 100644
--- a/src/ast/decl_collector.h
+++ b/src/ast/decl_collector.h
@@ -41,7 +41,7 @@ class decl_collector {
 
 public:
     // if preds == true, then predicates are stored in a separate collection.
-    decl_collector(ast_manager & m, bool preds=true);
+    decl_collector(ast_manager & m, bool preds = true);
     ast_manager & m() { return m_manager; }
 
     void visit_func(func_decl* n);