fix build

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

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());
         }
     }
 

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);
 

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();

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;