From ee2bae898a5d1dba52fac7058e979c8e3c026859 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 27 Jan 2016 18:09:24 +0000 Subject: [PATCH] remove unused exceeded_memory_allocations class --- src/util/memory_manager.h | 5 ----- 1 file changed, 5 deletions(-) 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();