Segmentation fault when using parallel instances of the bindings

Hi!

I'm encountering a segmentation fault when trying to run multiple instances of Bitwuzla in parallel using the Bitwuzla bindings with OCaml 5.1.1. When using the module instance provided by default in the bitwuzla-cxx library in a single-threaded context, everything works fine. However, issues arise when executing multiple instances concurrently.

Steps to Reproduce:

Consider the following small program:

let run () =
  let module M = Bitwuzla_cxx.Make () in
  let _ = M.mk_bool_sort () in
  true

let () =
  assert (
    Array.for_all Fun.id
      (Array.map Domain.join
        (Array.init (Domain.recommended_domain_count ()) (fun _ ->
              Domain.spawn run))))

When running this program, it generates a segmentation fault and crashes with the following backtrace:

Backtrace:

(gdb) run
Starting program: /home/filipe/code/ocaml-bitwuzla/_build/default/test/t_small.exe

This GDB supports auto-downloading debuginfo from the following URLs:
  <https://debuginfod.archlinux.org>
Enable debuginfod for this session? (y or [n]) y
Debuginfod has been enabled.
To make this setting permanent, add 'set debuginfod enabled on' to .gdbinit.
Downloading separate debug info for system-supplied DSO at 0x7ffff7fc7000
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/usr/lib/libthread_db.so.1".
[New Thread 0x7fffe76006c0 (LWP 380645)]
[New Thread 0x7fffe62006c0 (LWP 380647)]
[New Thread 0x7fffe6c006c0 (LWP 380646)]
[New Thread 0x7fffe58006c0 (LWP 380648)]

Thread 2 "t_small.exe" received signal SIGSEGV, Segmentation fault.
[Switching to Thread 0x7fffe76006c0 (LWP 380645)]
bzla::type::TypeManager::garbage_collect (this=0x7fffe001b, data=0x7fffe001ba20)
    at src/type/type_manager.cpp:153
153       d_in_gc_mode = true;
(gdb) backtrace
#0  bzla::type::TypeManager::garbage_collect (this=0x7fffe001b, data=0x7fffe001ba20)
    at src/type/type_manager.cpp:153
#1  0x00005555556da918 in bzla::type::TypeData::dec_ref (this=<optimized out>)
    at src/type/type_data.cpp:175
#2  0x00005555556da941 in bzla::Type::~Type (this=this@entry=0x7fffe001bb20,
    __in_chrg=<optimized out>) at src/type/type.cpp:26
#3  0x00005555556d3d92 in std::_Sp_counted_ptr<bzla::Type*, (__gnu_cxx::_Lock_policy)2>::_M_dispose (this=<optimized out>) at /usr/include/c++/14.1.1/bits/shared_ptr_base.h:428
#4  0x00005555556c22c1 in std::_Sp_counted_base<(__gnu_cxx::_Lock_policy)2>::_M_release (
    this=0x7fffe001bb40) at /usr/include/c++/14.1.1/bits/shared_ptr_base.h:346
#5  std::_Sp_counted_base<(__gnu_cxx::_Lock_policy)2>::_M_release (this=0x7fffe001bb40)
    at /usr/include/c++/14.1.1/bits/shared_ptr_base.h:317
#6  std::__shared_count<(__gnu_cxx::_Lock_policy)2>::~__shared_count (this=<optimized out>,
    __in_chrg=<optimized out>) at /usr/include/c++/14.1.1/bits/shared_ptr_base.h:1069
#7  std::__shared_ptr<bzla::Type, (__gnu_cxx::_Lock_policy)2>::~__shared_ptr (
    this=<optimized out>, __in_chrg=<optimized out>)
    at /usr/include/c++/14.1.1/bits/shared_ptr_base.h:1525
#8  std::shared_ptr<bzla::Type>::~shared_ptr (this=<optimized out>, __in_chrg=<optimized out>)
    at /usr/include/c++/14.1.1/bits/shared_ptr.h:175
#9  bitwuzla::Sort::~Sort (this=<optimized out>, __in_chrg=<optimized out>)
    at bitwuzla.cpp:1105
#10 0x00005555558c1c62 in custom_finalize_minor (domain=0x7fffe0002b80)
    at runtime/minor_gc.c:694
#11 caml_stw_empty_minor_heap_no_major_slice (domain=0x7fffe0002b80, participating_count=2,
    participating=<optimized out>, unused=<optimized out>) at runtime/minor_gc.c:743
#12 0x00005555558ae8e9 in caml_try_run_on_all_domains_with_spin_work (sync=sync@entry=1,
    handler=handler@entry=0x5555558c1ca0 <caml_stw_empty_minor_heap>, data=data@entry=0x0,
    leader_setup=leader_setup@entry=0x5555558c0a80 <caml_empty_minor_heap_setup>,
    enter_spin_callback=enter_spin_callback@entry=0x5555558c0c40 <caml_do_opportunistic_major_slice>, enter_spin_data=enter_spin_data@entry=0x0) at runtime/domain.c:1483
#13 0x00005555558c1db6 in caml_try_stw_empty_minor_heap_on_all_domains ()
    at runtime/minor_gc.c:799
#14 caml_empty_minor_heaps_once () at runtime/minor_gc.c:820
#15 0x00005555558adee2 in domain_terminate () at runtime/domain.c:1794
#16 domain_thread_func (v=<optimized out>) at runtime/domain.c:1106
#17 0x00007ffff79bbded in start_thread (arg=<optimized out>) at pthread_create.c:447
#18 0x00007ffff7a3f0dc in clone3 () at ../sysdeps/unix/sysv/linux/x86_64/clone3.S:78

Request

Am I using the bindings incorrectly? If so, could you guide me on the correct usage for running multiple instances in parallel?

Thanks!

Hi @filipeom,

Thank you for reporting this. Do you experience this with more complex examples ? For me, it looks like an unused type cause a segmentation fault when the term manager is destroyed.

@mpreiner @aniemetz I was able to reproduce it with the straight C++ API. Do you have any insight ?

#include <stdio.h>
#include <bitwuzla/cpp/bitwuzla.h>

using namespace bitwuzla;

int main (int argc, char *argv[])
{
  TermManager *tm = new TermManager();
  Sort sort = tm->mk_bool_sort();
  delete tm;
  return 0;
}

Program received signal SIGSEGV, Segmentation fault.
0x000055555563ad98 in bzla::type::TypeManager::garbage_collect(bzla::type::TypeData*) ()
(gdb) bt
#0  0x000055555563ad98 in bzla::type::TypeManager::garbage_collect(bzla::type::TypeData*) ()
#1  0x0000555555639cb5 in bzla::Type::~Type() ()
#2  0x00005555555aa466 in std::_Sp_counted_ptr<bzla::Type*, (__gnu_cxx::_Lock_policy)2>::_M_dispose() ()
#3  0x0000555555594152 in bitwuzla::Sort::~Sort() ()
#4  0x000055555558df89 in main ()

Regards, Frédéric

Do you experience this with more complex examples ?´

Yeah, I also experience it with the t_bitwuzla_cxx_5.ml example in this repository, but I wasn't able to pinpoint exactly where it happens (See Backtrace below)

We also run it normally here, and I guess the bool_sort is also never used defined here, but there's no issue there.

Backtrace:

[New Thread 0x7fffe76006c0 (LWP 429641)]
[New Thread 0x7fffe62006c0 (LWP 429643)]
[New Thread 0x7fffe6c006c0 (LWP 429642)]
[New Thread 0x7fffe58006c0 (LWP 429644)]
[New Thread 0x7fffdfe006c0 (LWP 429646)]
[New Thread 0x7fffe4e006c0 (LWP 429645)]
[New Thread 0x7fffdf4006c0 (LWP 429647)]
[New Thread 0x7fffdea006c0 (LWP 429648)]
[New Thread 0x7fffde0006c0 (LWP 429649)]
[New Thread 0x7fffdd6006c0 (LWP 429650)]
[New Thread 0x7fffdcc006c0 (LWP 429651)]
[New Thread 0x7fffd3e006c0 (LWP 429652)]
[New Thread 0x7fffd34006c0 (LWP 429653)]
[New Thread 0x7fffd2a006c0 (LWP 429654)]
[New Thread 0x7fffd16006c0 (LWP 429656)]
[New Thread 0x7fffd20006c0 (LWP 429655)]
[New Thread 0x7fffd0c006c0 (LWP 429657)]

Thread 5 "t_bitwuzla.exe" received signal SIGSEGV, Segmentation fault.
[Switching to Thread 0x7fffe58006c0 (LWP 429644)]
bzla::NodeManager::garbage_collect (this=0x7ff827f9d43e, data=0x7fffd802e630) at src/node/node_manager.cpp:844
844       d_in_gc_mode = true;
(gdb) backtrace
#0  bzla::NodeManager::garbage_collect (this=0x7ff827f9d43e, data=0x7fffd802e630) at src/node/node_manager.cpp:844
#1  0x00005555557611fb in bzla::node::NodeData::gc (this=<optimized out>) at src/node/node_data.cpp:222
#2  0x0000555555761219 in bzla::node::NodeData::dec_ref (this=<optimized out>) at src/node/node_data.h:202
#3  bzla::Node::~Node (this=this@entry=0x7fffd80226f8, __in_chrg=<optimized out>) at src/node/node.cpp:33
#4  0x000055555578a94d in std::pair<bzla::Node const, std::vector<bzla::bitblast::AigNode, std::allocator<bzla::bitblast::AigNode> > >::~pair (this=0x7fffd80226f8, __in_chrg=<optimized out>)
    at /usr/include/c++/14.1.1/bits/new_allocator.h:104
#5  std::__new_allocator<std::__detail::_Hash_node<std::pair<bzla::Node const, std::vector<bzla::bitblast::AigNode, std::allocator<bzla::bitblast::AigNode> > >, true> >::destroy<std::pair<bzla::Node const, std::vector<bzla::bitblast::AigNode, std::allocator<bzla::bitblast::AigNode> > > > (this=<optimized out>, __p=0x7fffd80226f8)
    at /usr/include/c++/14.1.1/bits/new_allocator.h:198
#6  std::allocator_traits<std::allocator<std::__detail::_Hash_node<std::pair<bzla::Node const, std::vector<bzla::bitblast::AigNode, std::allocator<bzla::bitblast::AigNode> > >, true> > >::destroy<std::pair<bzla::Node const, std::vector<bzla::bitblast::AigNode, std::allocator<bzla::bitblast::AigNode> > > > (__a=..., __p=0x7fffd80226f8)
    at /usr/include/c++/14.1.1/bits/alloc_traits.h:554
#7  std::__detail::_Hashtable_alloc<std::allocator<std::__detail::_Hash_node<std::pair<bzla::Node const, std::vector<bzla::bitblast::AigNode, std::allocator<bzla::bitblast::AigNode> > >, true> > >::_M_deallocate_node (this=0x7fffd801f9d8, __n=0x7fffd80226f0) at /usr/include/c++/14.1.1/bits/hashtable_policy.h:2040
#8  std::__detail::_Hashtable_alloc<std::allocator<std::__detail::_Hash_node<std::pair<bzla::Node const, std::vector<bzla::bitblast::AigNode, std::allocator<bzla::bitblast::AigNode> > >, true> > >::_M_deallocate_nodes (this=0x7fffd801f9d8, __n=0x7fffd802efb0) at /usr/include/c++/14.1.1/bits/hashtable_policy.h:2062
#9  std::_Hashtable<bzla::Node, std::pair<bzla::Node const, std::vector<bzla::bitblast::AigNode, std::allocator<bzla::bitblast::AigNode> > >, std::allocator<std::pair<bzla::Node const, std::vector<bzla::bitblast::AigNode, std::allocator<bzla::bitblast::AigNode> > > >, std::__detail::_Select1st, std::equal_to<bzla::Node>, std::hash<bzla::Node>, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<true, false, true> >::clear (this=0x7fffd801f9d8)
    at /usr/include/c++/14.1.1/bits/hashtable.h:2584
#10 std::_Hashtable<bzla::Node, std::pair<bzla::Node const, std::vector<bzla::bitblast::AigNode, std::allocator<bzla::bitblast::AigNode> > >, std::allocator<std::pair<bzla::Node const, std::vector<bzla::bitblast::AigNode, std::allocator<bzla::bitblast::AigNode> > > >, std::__detail::_Select1st, std::equal_to<bzla::Node>, std::hash<bzla::Node>, std::__detail::_Mod_range_hashing, std::__detail::_Default_ranged_hash, std::__detail::_Prime_rehash_policy, std::__detail::_Hashtable_traits<true, false, true> >::~_Hashtable (this=0x7fffd801f9d8, __in_chrg=<optimized out>)
    at /usr/include/c++/14.1.1/bits/hashtable.h:1667
#11 std::unordered_map<bzla::Node, std::vector<bzla::bitblast::AigNode, std::allocator<bzla::bitblast::AigNode> >, std::hash<bzla::Node>, std::equal_to<bzla::Node>, std::allocator<std::pair<bzla::Node const, std::vector<bzla::bitblast::AigNode, std::allocator<bzla::bitblast::AigNode> > > > >::~unordered_map (this=0x7fffd801f9d8, __in_chrg=<optimized out>)
    at /usr/include/c++/14.1.1/bits/unordered_map.h:109
#12 bzla::bv::AigBitblaster::~AigBitblaster (this=0x7fffd801f938, __in_chrg=<optimized out>) at src/solver/bv/aig_bitblaster.h:22
#13 bzla::bv::BvBitblastSolver::~BvBitblastSolver (this=this@entry=0x7fffd801f858, __in_chrg=<optimized out>) at src/solver/bv/bv_bitblast_solver.cpp:66
#14 0x00005555557858e0 in bzla::bv::BvSolver::~BvSolver (this=this@entry=0x7fffd801f7f0, __in_chrg=<optimized out>) at src/solver/bv/bv_solver.cpp:63
#15 0x0000555555722639 in bzla::SolverEngine::~SolverEngine (this=0x7fffd801f548, __in_chrg=<optimized out>) at src/solver/solver_engine.h:45
#16 0x000055555571d39d in bzla::SolvingContext::~SolvingContext (this=0x7fffd801db80, __in_chrg=<optimized out>) at src/solving_context.cpp:42
#17 0x000055555570078c in std::default_delete<bzla::SolvingContext>::operator() (this=<optimized out>, __ptr=0x7fffd801db80) at /usr/include/c++/14.1.1/bits/unique_ptr.h:87
#18 std::default_delete<bzla::SolvingContext>::operator() (this=<optimized out>, __ptr=0x7fffd801db80) at /usr/include/c++/14.1.1/bits/unique_ptr.h:87
#19 std::unique_ptr<bzla::SolvingContext, std::default_delete<bzla::SolvingContext> >::~unique_ptr (this=0x7fffd801daf0, __in_chrg=<optimized out>)
    at /usr/include/c++/14.1.1/bits/unique_ptr.h:398
#20 bitwuzla::Bitwuzla::~Bitwuzla (this=this@entry=0x7fffd801daf0, __in_chrg=<optimized out>) at bitwuzla.cpp:1338
#21 0x00005555556e8433 in internal_bitwuzla_delete (vt=<optimized out>) at cxx_stubs.cpp:1542
#22 0x000055555590c2b2 in custom_finalize_minor (domain=0x7fffd8002b80) at runtime/minor_gc.c:694
#23 caml_stw_empty_minor_heap_no_major_slice (domain=0x7fffd8002b80, participating_count=9, participating=<optimized out>, unused=<optimized out>) at runtime/minor_gc.c:743
#24 0x00005555558f81a9 in caml_try_run_on_all_domains_with_spin_work (sync=sync@entry=1, handler=handler@entry=0x55555590c2f0 <caml_stw_empty_minor_heap>, data=data@entry=0x0,
    leader_setup=leader_setup@entry=0x55555590b0d0 <caml_empty_minor_heap_setup>, enter_spin_callback=enter_spin_callback@entry=0x55555590b290 <caml_do_opportunistic_major_slice>,
    enter_spin_data=enter_spin_data@entry=0x0) at runtime/domain.c:1483
#25 0x000055555590c406 in caml_try_stw_empty_minor_heap_on_all_domains () at runtime/minor_gc.c:799
#26 caml_empty_minor_heaps_once () at runtime/minor_gc.c:820
#27 0x00005555558f77a2 in domain_terminate () at runtime/domain.c:1794
#28 domain_thread_func (v=<optimized out>) at runtime/domain.c:1106
#29 0x00007ffff79bbded in start_thread (arg=<optimized out>) at pthread_create.c:447
--Type <RET> for more, q to quit, c to continue without paging--
#30 0x00007ffff7a3f0dc in clone3 () at ../sysdeps/unix/sysv/linux/x86_64/clone3.S:78

I guess it is related to the fact that the TermManager is deleted before the Sort node it creates.

For instance, the following small variation works fine.

int main (int argc, char *argv[])
{
  TermManager *tm = new TermManager();
  {
    Sort sort = tm->mk_bool_sort();
  }
  delete tm;
  return 0;
}

It is visible and racy in OCaml because of the automatic garbage collector (especially with multiple domains). Indeed, OCaml values are deallocated in an arbitrary order when both values are unreachable when the GC triggers. The issue does not raise with the default term constructors, since the underlying NodeManager is never deallocated.

As a workaround in the OCaml side, you can use the following.

diff --git a/bitwuzla_cxx.ml b/bitwuzla_cxx.ml
index 24bdc86d2eb..deafdb5dd95 100644
--- a/bitwuzla_cxx.ml
+++ b/bitwuzla_cxx.ml
@@ -1911,6 +1911,7 @@ end

 module Make () : S = struct
   let t = Manager.create ()
+  let () = Gc.finalise (fun t -> ignore (ref t)) t

   module Sort = Sort

It delays by one round the collection of the TermManager .

As a workaround in the OCaml side, you can use the following.

Yes, it seems to no longer be crashing :smile: Thanks!

Hi @filipeom,

Thank you for reporting this. Do you experience this with more complex examples ? For me, it looks like an unused type cause a segmentation fault when the term manager is destroyed.

@mpreiner @aniemetz I was able to reproduce it with the straight C++ API. Do you have any insight ?
#include <stdio.h>
#include <bitwuzla/cpp/bitwuzla.h>

using namespace bitwuzla;

int main (int argc, char *argv[])
{
  TermManager *tm = new TermManager();
  Sort sort = tm->mk_bool_sort();
  delete tm;
  return 0;
}
Program received signal SIGSEGV, Segmentation fault.
0x000055555563ad98 in bzla::type::TypeManager::garbage_collect(bzla::type::TypeData*) ()
(gdb) bt
#0  0x000055555563ad98 in bzla::type::TypeManager::garbage_collect(bzla::type::TypeData*) ()
#1  0x0000555555639cb5 in bzla::Type::~Type() ()
#2  0x00005555555aa466 in std::_Sp_counted_ptr<bzla::Type*, (__gnu_cxx::_Lock_policy)2>::_M_dispose() ()
#3  0x0000555555594152 in bitwuzla::Sort::~Sort() ()
#4  0x000055555558df89 in main ()
Regards, Frédéric

This is expected behavior if you delete the term manager before all created terms/sorts are destroyed. You have to make sure that the term manager is destroyed after all terms/sorts are destroyed.

This is expected behavior if you delete the term manager before all created terms/sorts are destroyed. You have to make sure that the term manager is destroyed after all terms/sorts are destroyed.

Ok, so would you accept a tentative fix using something similar to z3 ctx object counting to solve this issue?

@mpreiner @aniemetz Is there an easy way to make sure that no Sort or Term of a given TermManager is still alive ? (like a counter in the internal structure ?) I would be sad to have to implement a reference counting on every exported types for a rare race condition, especially when a similar task is already performed elsewhere.

The issue here is that at the point where the Sort is destroyed, the underlying data is already deleted. The term manager (or internally node and type manager) manage all created terms and sorts. If a sort/term is destructed, it gets deleted in the corresponding node/type manager. However, if the node/type manager is already destroyed, the pointer pointing to the node data (from which we retrieve the node/type manager) is already invalid. There is no easy way on our side to track all the references for nodes/types since we'd have to keep track of every external reference (i.e. Term and Sort object), which is not feasible. The only way I can think of is to just not destroy the internal node manager if there are still sorts/types around, but if possible I'd like to avoid this since this usually points to a misuse of the API and would leak memory since the internal node manager would not be destroyed.

The correct way to fix your above example would be:

int main (int argc, char *argv[])
{
  std::unique_ptr<TermManager> tm (new TermManager());
  Sort sort = tm->mk_bool_sort();
  return 0;
}

int main (int argc, char *argv[])
{
  TermManager tm;
  Sort sort = tm.mk_bool_sort();
  return 0;
}

This would ensure the correct destruction order of the term manager and the objects that depend on it. Why is it not possible to enforce the proper destruction order of objects on the OCaml side?

Further note, that the current API of the term manager is not reentrant. So using the same term manager in different threads is not supported.

Thank you @mpreiner I understand how the API should be used at C++ level, but there is no equivalent at OCaml level. Term, Sort, TermManager (, etc.) are exported as custom blocks that are managed by the Garbage Collector.

The typing rules make it impossible to use a Term if the corresponding TermManager is no longer alive. This is correct by construction.

However, both Term and TermManager may become unreachable during the same GC round and then, we have no guarantee on which one will be collected first.

I could eventually make add a shared_ptr to each OCaml object so TermManager will be deleted only once every created nodes are collected. Yet, it would be quite heavy, especially since another mechanism already exists.

The point is that NodeManager (internal structure) is shared : each internal Node has a pointer to it, and it has a storage to all nodes. So here is the way I would proceed:

add a "delete request" function in the API of NodeManager;
change std::unique_ptr<bzla::NodeManager> d_nm; to simple pointer in TermManager, call "delete request" in TermManager destructor;
when called "delete request", if NodeManager is empty then delete this, else, set a flag "delete requested";
each time a Node is collected, if "delete requested" is set and the NodeManager is empty then delete this else, continue as usual.

(Do we reimplement the logic of shared pointer ? Not exactly, but there are a lot of similarities.)

Regarding storing a reference in Term/Sort for proper destruction order. We are doing the same for the Python API to ensure proper destruction order in the Python GC. If you think that this may be too much overhead on the OCaml side, you could also just not delete the term manager (and leak memory).

I'm hesitant to add language-specific workarounds in the core of the solver if it can be avoided. It can still get quite messy with a flag that indicates whether the node manager needs to be destroyed or not, especially if shared between multiple solver instances.

I disagree with the "language-specific" workaround. Doing what I described not only would help OCaml side, but may also help the Python side and will actually make the C++ API safer. What I propose is more or less just a reference counting in the internal NodeManager structure instead of doing this in all the wrappers. To me, it sounds safer, easier and more efficient to do this at this level.

Replace the "delete requested" by d_refs, increments/decrements it each time a NodeData/TypeData/Bitwuzla/TermManager is created/deleted. When reach 0, delete the NodeManager. Sound pretty easy, almost 0 overhead.

(Note, I can try to propose a patch if you mind)

As an example of what can be done.

diff --git a/include/bitwuzla/cpp/bitwuzla.h b/include/bitwuzla/cpp/bitwuzla.h
index e3024d5c..8bb4f456 100644
--- a/include/bitwuzla/cpp/bitwuzla.h
+++ b/include/bitwuzla/cpp/bitwuzla.h
@@ -1451,7 +1451,7 @@ class TermManager

  private:
-  std::unique_ptr<bzla::NodeManager> d_nm;
+  bzla::NodeManager *d_nm;
 };

 /* -------------------------------------------------------------------------- */
@@ -1639,9 +1639,6 @@ class Bitwuzla
    */
   std::map<std::string, std::string> statistics() const;

-  /** @return The associated term manager instance. */
-  TermManager &term_mgr();
-
  private:
   /** Helper called when solver state changes. */
   void solver_state_change();
@@ -1664,8 +1661,8 @@ class Bitwuzla
   bool d_uc_is_valid = false;
   /** Indicates a pending pop from check-sat with assumptions. */
   bool d_pending_pop = false;
-  /** The associated term manager instance. */
-  TermManager &d_tm;
+  /** The associated node manager instance. */
+  bzla::NodeManager *d_nm;
 };

 /* -------------------------------------------------------------------------- */
diff --git a/src/api/checks.h b/src/api/checks.h
index d19ca211..f4a3033c 100644
--- a/src/api/checks.h
+++ b/src/api/checks.h
@@ -98,7 +98,7 @@ class BitwuzlaExceptionStream
 #define BITWUZLA_CHECK_TERM_TERM_MGR(term, what)    \
   do                                                \
   {                                                 \
-    BITWUZLA_CHECK(d_nm.get() == term.d_node->nm()) \
+    BITWUZLA_CHECK(d_nm == term.d_node->nm())       \
         << "mismatching term manager for " << what; \
   } while (0)

@@ -261,7 +261,7 @@ class BitwuzlaExceptionStream
     for (size_t i = 0, argc = args.size(); i < argc; ++i)                      \
     {                                                                          \
       BITWUZLA_CHECK_NOT_NULL_AT_IDX(args[i].d_node, i);                       \
-      BITWUZLA_CHECK(d_nm.get() == args[i].d_node->nm())                       \
+      BITWUZLA_CHECK(d_nm == args[i].d_node->nm())                             \
           << "mismatching term manager for term at index " << i;               \
       if (i == start || i > start)                                             \
       {                                                                        \
diff --git a/src/api/cpp/bitwuzla.cpp b/src/api/cpp/bitwuzla.cpp
index 4991b68d..5503fa38 100644
--- a/src/api/cpp/bitwuzla.cpp
+++ b/src/api/cpp/bitwuzla.cpp
@@ -1331,11 +1331,15 @@ class TerminatorInternal : public bzla::Terminator

 Bitwuzla::Bitwuzla(TermManager &tm, const Options &options)
     : d_ctx(new bzla::SolvingContext(*tm.d_nm, *options.d_options, "main")),
-      d_tm(tm)
+      d_nm(tm.d_nm)
 {
+  d_nm->inc_ref();
 }

-Bitwuzla::~Bitwuzla() {}
+Bitwuzla::~Bitwuzla()
+{
+  d_nm->dec_ref();
+}

 void
 Bitwuzla::configure_terminator(Terminator *terminator)
@@ -1542,12 +1546,6 @@ Bitwuzla::statistics() const
   return d_ctx->env().statistics().get();
 }

-TermManager &
-Bitwuzla::term_mgr()
-{
-  return d_tm;
-}
-
 /* Bitwuzla private --------------------------------------------------------- */

 void
@@ -1562,9 +1560,15 @@ Bitwuzla::solver_state_change()

 /* TermManager public ------------------------------------------------------- */

-TermManager::TermManager() : d_nm(new bzla::NodeManager()) {}
+TermManager::TermManager() : d_nm(new bzla::NodeManager())
+{
+  d_nm->inc_ref();
+}

-TermManager::~TermManager() {}
+TermManager::~TermManager()
+{
+  d_nm->dec_ref();
+}

 Sort
 TermManager::mk_array_sort(const Sort &index, const Sort &element)
diff --git a/src/node/node_manager.cpp b/src/node/node_manager.cpp
index fec44f4c..9011d88e 100644
--- a/src/node/node_manager.cpp
+++ b/src/node/node_manager.cpp
@@ -41,14 +41,14 @@ NodeManager::~NodeManager()
 type::TypeManager*
 NodeManager::tm()
 {
-  return &d_tm;
+  return this;
 }

 Node
 NodeManager::mk_const(const Type& t, const std::optional<std::string>& symbol)
 {
   assert(!t.is_null());
-  assert(t.tm() == &d_tm);
+  assert(t.tm() == this);
   NodeData* data = NodeData::alloc(Kind::CONSTANT, symbol);
   data->d_type   = t;
   init_id(data);
@@ -63,7 +63,7 @@ NodeManager::mk_const_array(const Type& t, const Node& term)
   assert(!term.is_null());
   assert(t.is_array());
   assert(t.array_element() == term.type());
-  assert(t.tm() == &d_tm);
+  assert(t.tm() == this);
   assert(term.nm() == this);

   NodeData* data = find_or_insert_node(Kind::CONST_ARRAY, t, {term}, {});
@@ -74,7 +74,7 @@ Node
 NodeManager::mk_var(const Type& t, const std::optional<std::string>& symbol)
 {
   assert(!t.is_null());
-  assert(t.tm() == &d_tm);
+  assert(t.tm() == this);
   NodeData* data = NodeData::alloc(Kind::VARIABLE, symbol);
   data->d_type   = t;
   init_id(data);
@@ -167,43 +167,43 @@ NodeManager::invert_node(const Node& node)
 Type
 NodeManager::mk_bool_type()
 {
-  return d_tm.mk_bool_type();
+  return TypeManager::mk_bool_type();
 }

 Type
 NodeManager::mk_bv_type(uint64_t size)
 {
-  return d_tm.mk_bv_type(size);
+  return TypeManager::mk_bv_type(size);
 }

 Type
 NodeManager::mk_fp_type(uint64_t exp_size, uint64_t sig_size)
 {
-  return d_tm.mk_fp_type(exp_size, sig_size);
+  return TypeManager::mk_fp_type(exp_size, sig_size);
 }

 Type
 NodeManager::mk_rm_type()
 {
-  return d_tm.mk_rm_type();
+  return TypeManager::mk_rm_type();
 }

 Type
 NodeManager::mk_array_type(const Type& index, const Type& elem)
 {
-  return d_tm.mk_array_type(index, elem);
+  return TypeManager::mk_array_type(index, elem);
 }

 Type
 NodeManager::mk_fun_type(const std::vector<Type>& types)
 {
-  return d_tm.mk_fun_type(types);
+  return TypeManager::mk_fun_type(types);
 }

 Type
 NodeManager::mk_uninterpreted_type(const std::optional<std::string>& symbol)
 {
-  return d_tm.mk_uninterpreted_type(symbol);
+  return TypeManager::mk_uninterpreted_type(symbol);
 }

 Type
@@ -268,29 +268,29 @@ NodeManager::compute_type(Kind kind,
     case Kind::FP_IS_SUBNORMAL:
     case Kind::FP_IS_ZERO:
     case Kind::FORALL:
-    case Kind::EXISTS: return d_tm.mk_bool_type();
+    case Kind::EXISTS: return TypeManager::mk_bool_type();

     case Kind::BV_EXTRACT: {
       uint64_t upper = indices[0];
       uint64_t lower = indices[1];
-      return d_tm.mk_bv_type(upper - lower + 1);
+      return TypeManager::mk_bv_type(upper - lower + 1);
     }

     case Kind::BV_REPEAT:
-      return d_tm.mk_bv_type(children[0].type().bv_size() * indices[0]);
+      return TypeManager::mk_bv_type(children[0].type().bv_size() * indices[0]);

     case Kind::BV_SIGN_EXTEND:
     case Kind::BV_ZERO_EXTEND:
-      return d_tm.mk_bv_type(children[0].type().bv_size() + indices[0]);
+      return TypeManager::mk_bv_type(children[0].type().bv_size() + indices[0]);

     case Kind::BV_CONCAT:
-      return d_tm.mk_bv_type(children[0].type().bv_size()
-                             + children[1].type().bv_size());
+      return TypeManager::mk_bv_type(children[0].type().bv_size()
+                    + children[1].type().bv_size());

     case Kind::BV_COMP:
     case Kind::BV_REDAND:
     case Kind::BV_REDOR:
-    case Kind::BV_REDXOR: return d_tm.mk_bv_type(1);
+    case Kind::BV_REDXOR: return TypeManager::mk_bv_type(1);

     case Kind::BV_ADD:
     case Kind::BV_AND:
@@ -334,16 +334,16 @@ NodeManager::compute_type(Kind kind,
     case Kind::ITE: return children[1].type();

     case Kind::FP_FP:
-      return d_tm.mk_fp_type(children[1].type().bv_size(),
-                             children[2].type().bv_size() + 1);
+      return TypeManager::mk_fp_type(children[1].type().bv_size(),
+                    children[2].type().bv_size() + 1);
     case Kind::FP_TO_SBV:
-    case Kind::FP_TO_UBV: return d_tm.mk_bv_type(indices[0]);
+    case Kind::FP_TO_UBV: return TypeManager::mk_bv_type(indices[0]);

     case Kind::FP_TO_FP_FROM_BV:
     case Kind::FP_TO_FP_FROM_FP:
     case Kind::FP_TO_FP_FROM_SBV:
     case Kind::FP_TO_FP_FROM_UBV:
-      return d_tm.mk_fp_type(indices[0], indices[1]);
+      return TypeManager::mk_fp_type(indices[0], indices[1]);

     case Kind::SELECT: return children[0].type().array_element();

@@ -361,7 +361,7 @@ NodeManager::compute_type(Kind kind,
       {
         types.push_back(children[1].type());
       }
-      return d_tm.mk_fun_type(types);
+      return TypeManager::mk_fun_type(types);
     }
   }

@@ -809,6 +809,7 @@ NodeManager::init_id(NodeData* data)
   data->d_id = d_node_id_counter++;
   data->d_nm = this;
   ++d_stats.d_num_node_data;
+  ++d_refs;
 }

 NodeData*
@@ -886,9 +887,12 @@ NodeManager::garbage_collect(NodeData* data)
     NodeData::dealloc(cur);
     --d_stats.d_num_node_data;
     ++d_stats.d_num_node_data_dealloc;
+    --d_refs;
   } while (!visit.empty());

   d_in_gc_mode = false;
+
+  check_refs();
 }

 const std::optional<std::reference_wrapper<const std::string>>
@@ -903,4 +907,9 @@ NodeManager::get_symbol(const NodeData* data) const
       payload.d_symbol};
 }

+void
+NodeManager::inc_ref() { TypeManager::inc_ref(); }
+void
+NodeManager::dec_ref() { TypeManager::dec_ref(); }
+
 }  // namespace bzla
diff --git a/src/node/node_manager.h b/src/node/node_manager.h
index a4490213..9bd674e6 100644
--- a/src/node/node_manager.h
+++ b/src/node/node_manager.h
@@ -31,7 +31,7 @@ class BitVector;
 class FloatingPoint;
 enum class RoundingMode;

-class NodeManager
+class NodeManager : protected type::TypeManager
 {
   friend node::NodeData;

@@ -191,6 +191,17 @@ class NodeManager
   uint64_t max_node_id() const { return d_node_id_counter; }
 #endif

+  /** Increase the reference count by one. */
+  void inc_ref();
+
+  /**
+   * Decrease the reference count by one.
+   *
+   * If reference count becomes zero, this node manager object will be
+   * automatically garbage collected.
+   */
+  void dec_ref();
+
   const auto& statistics() const { return d_stats; }

  private:
@@ -236,9 +247,6 @@ class NodeManager
   const std::optional<std::reference_wrapper<const std::string>> get_symbol(
       const node::NodeData* d) const;

-  /** Type manager. */
-  type::TypeManager d_tm;
-
   /** Node id counter. */
   uint64_t d_node_id_counter = 1;

diff --git a/src/type/type_manager.cpp b/src/type/type_manager.cpp
index 3a2d1672..588dcd54 100644
--- a/src/type/type_manager.cpp
+++ b/src/type/type_manager.cpp
@@ -104,6 +104,7 @@ TypeManager::init_id(TypeData* data)
   d_node_data.emplace_back(data);
   assert(d_node_data.size() == static_cast<size_t>(d_type_id_counter));
   data->d_id = d_type_id_counter++;
+  d_refs++;
 }

 TypeData*
@@ -186,9 +187,29 @@ TypeManager::garbage_collect(TypeData* data)

     assert(d_node_data[cur->d_id - 1]->d_id == cur->d_id);
     d_node_data[cur->d_id - 1].reset(nullptr);
+    d_refs--;
   } while (!visit.empty());

   d_in_gc_mode = false;
+
+  check_refs();
+}
+
+void
+TypeManager::check_refs()
+{
+  if (d_refs == 0)
+    {
+      delete this;
+    }
+}
+
+void
+TypeManager::dec_ref()
+{
+  assert(d_refs > 0);
+  --d_refs;
+  check_refs();
 }

 }  // namespace bzla::type
diff --git a/src/type/type_manager.h b/src/type/type_manager.h
index 19f9597c..a86e6840 100644
--- a/src/type/type_manager.h
+++ b/src/type/type_manager.h
@@ -29,7 +29,7 @@ class TypeManager
   friend TypeData;

  public:
-  ~TypeManager();
+  virtual ~TypeManager();

   /**
    * @return Boolean type.
@@ -84,6 +84,26 @@ class TypeManager
   Type mk_uninterpreted_type(
       const std::optional<std::string>& symbol = std::nullopt);

+  /** Increase the reference count by one. */
+  void inc_ref() { ++d_refs; }
+
+  /**
+   * Decrease the reference count by one.
+   *
+   * If reference count becomes zero, this type manager object will be
+   * automatically garbage collected.
+   */
+  void dec_ref();
+
+ protected:
+  /**
+   * If reference count is zero, this type manager object will be
+   * garbage collected.
+   */
+  void check_refs();
+  /** Number of references. */
+  uint32_t d_refs = 0;
+
  private:
   /** Initialize type data. */
   void init_id(TypeData* d);

Hi @mpreiner, what do you think about the changes? Is there a chance something similar to be pushed in a future release?

Sorry, didn't have time to look into this yet, I'm too busy right now, but it's on my TODO list.

bitwuzla / ocaml-bitwuzla