From be33bb7b48588cf53cd1e6d0450931f798773334 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 8 Oct 2019 12:19:54 -0700
Subject: [PATCH] fix build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/api_solver.cpp     | 4 +++-
 src/ast/ast_pp_util.h      | 2 +-
 src/ast/decl_collector.cpp | 5 +++++
 src/ast/decl_collector.h   | 1 +
 4 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index b526b32ed..93e979016 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -77,7 +77,9 @@ extern "C" {
 
     solver2smt2_pp::solver2smt2_pp(ast_manager& m, char const* file): m_pp_util(m), m_out(file) {
         if (!m_out) {
-            throw default_exception("could not open file for output");
+            std::string msg;
+            msg = msg + "could not open " + file + " for output";
+            throw default_exception(msg.c_str());
         }
     }
 
diff --git a/src/ast/ast_pp_util.h b/src/ast/ast_pp_util.h
index fb0609968..d4f65b975 100644
--- a/src/ast/ast_pp_util.h
+++ b/src/ast/ast_pp_util.h
@@ -33,7 +33,7 @@ class ast_pp_util {
 
     decl_collector      coll;
 
- ast_pp_util(ast_manager& m): m(m), m_env(m), coll(m), m_num_sorts(0), m_num_decls(0) {}
+    ast_pp_util(ast_manager& m): m(m), m_env(m), m_num_sorts(0), m_num_decls(0), coll(m) {}
 
     void collect(expr* e);
 
diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp
index 7ddc8bd3d..dc0ea6bdc 100644
--- a/src/ast/decl_collector.cpp
+++ b/src/ast/decl_collector.cpp
@@ -53,18 +53,23 @@ void decl_collector::visit_func(func_decl * n) {
             m_decls.push_back(n);
         }
         m_visited.mark(n, true);
+        m_trail.push_back(n);
     }
 }
 
 decl_collector::decl_collector(ast_manager & m):
     m_manager(m),
+    m_trail(m),
     m_dt_util(m) {
     m_basic_fid = m_manager.get_basic_family_id();
     m_dt_fid = m_dt_util.get_family_id();
 }
 
 void decl_collector::visit(ast* n) {
+    if (m_visited.is_marked(n)) 
+        return;
     datatype_util util(m());
+    m_trail.push_back(n);
     m_todo.push_back(n);
     while (!m_todo.empty()) {
         n = m_todo.back();
diff --git a/src/ast/decl_collector.h b/src/ast/decl_collector.h
index b103b58d0..29e47cab4 100644
--- a/src/ast/decl_collector.h
+++ b/src/ast/decl_collector.h
@@ -29,6 +29,7 @@ class decl_collector {
     ptr_vector<sort>      m_sorts;
     ptr_vector<func_decl> m_decls;
     ast_mark              m_visited;
+    ast_ref_vector        m_trail;
     family_id             m_basic_fid;
     family_id             m_dt_fid;
     datatype_util         m_dt_util;