diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h index 34aee9d6e..b6831faa7 100644 --- a/src/util/memory_manager.h +++ b/src/util/memory_manager.h @@ -46,11 +46,6 @@ public: out_of_memory_error(); }; -class exceeded_memory_allocations : public z3_error { -public: - exceeded_memory_allocations(); -}; - class memory { public: static bool is_out_of_memory();