diff --git a/src/api/api_algebraic.cpp b/src/api/api_algebraic.cpp
index bee39aa2a..2e14a1bd8 100644
--- a/src/api/api_algebraic.cpp
+++ b/src/api/api_algebraic.cpp
@@ -378,7 +378,7 @@ extern "C" {
             vector_var2anum v2a(as);
             _am.isolate_roots(_p, v2a, roots);
         }
-        Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, mk_c(c)->m());
+        Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
         mk_c(c)->save_object(result);
         for (unsigned i = 0; i < roots.size(); i++) {
             result->m_ast_vector.push_back(au(c).mk_numeral(roots.get(i), false));
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index cfe082802..9955cbc8f 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -721,7 +721,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_simplify_get_param_descrs(c);
         RESET_ERROR_CODE();
-        Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref);
+        Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c));
         mk_c(c)->save_object(d);
         th_rewriter::get_param_descrs(d->m_descrs);
         Z3_param_descrs r = of_param_descrs(d);
diff --git a/src/api/api_ast_map.cpp b/src/api/api_ast_map.cpp
index d9e08ec3e..aa52faa98 100644
--- a/src/api/api_ast_map.cpp
+++ b/src/api/api_ast_map.cpp
@@ -34,7 +34,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_ast_map(c);
         RESET_ERROR_CODE();
-        Z3_ast_map_ref * m = alloc(Z3_ast_map_ref, mk_c(c)->m());
+        Z3_ast_map_ref * m = alloc(Z3_ast_map_ref, *mk_c(c), mk_c(c)->m());
         mk_c(c)->save_object(m);
         Z3_ast_map r       = of_ast_map(m);
         RETURN_Z3(r);
@@ -137,7 +137,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_ast_map_keys(c, m);
         RESET_ERROR_CODE();
-        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, to_ast_map(m)->m);
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), to_ast_map(m)->m);
         mk_c(c)->save_object(v);
         obj_map<ast, ast*>::iterator it  = to_ast_map_ref(m).begin();
         obj_map<ast, ast*>::iterator end = to_ast_map_ref(m).end();
diff --git a/src/api/api_ast_map.h b/src/api/api_ast_map.h
index 8e4f24623..dc1cf90ad 100644
--- a/src/api/api_ast_map.h
+++ b/src/api/api_ast_map.h
@@ -24,7 +24,7 @@ Revision History:
 struct Z3_ast_map_ref : public api::object {
     ast_manager &            m;
     obj_map<ast, ast*> m_map;
-    Z3_ast_map_ref(ast_manager & _m):m(_m) {}
+    Z3_ast_map_ref(api::context& c, ast_manager & _m): api::object(c), m(_m) {}
     virtual ~Z3_ast_map_ref();
 };
 
diff --git a/src/api/api_ast_vector.cpp b/src/api/api_ast_vector.cpp
index e1d4d78ff..5a1d974c1 100644
--- a/src/api/api_ast_vector.cpp
+++ b/src/api/api_ast_vector.cpp
@@ -29,7 +29,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_ast_vector(c);
         RESET_ERROR_CODE();
-        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
         mk_c(c)->save_object(v);
         Z3_ast_vector r       = of_ast_vector(v);
         RETURN_Z3(r);
@@ -111,7 +111,7 @@ extern "C" {
             RETURN_Z3(0);
         }
         ast_translation translator(mk_c(c)->m(), mk_c(t)->m()); 
-        Z3_ast_vector_ref * new_v = alloc(Z3_ast_vector_ref, mk_c(t)->m());
+        Z3_ast_vector_ref * new_v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(t)->m());
         mk_c(t)->save_object(new_v);
         unsigned sz = to_ast_vector_ref(v).size();
         for (unsigned i = 0; i < sz; i++) {
diff --git a/src/api/api_ast_vector.h b/src/api/api_ast_vector.h
index 20efa21c5..4fcf8ffb8 100644
--- a/src/api/api_ast_vector.h
+++ b/src/api/api_ast_vector.h
@@ -20,9 +20,13 @@ Revision History:
 
 #include"api_util.h"
 
+namespace api {
+    class context;
+};
+
 struct Z3_ast_vector_ref : public api::object {
     ast_ref_vector  m_ast_vector;
-    Z3_ast_vector_ref(ast_manager & m):m_ast_vector(m) {}
+    Z3_ast_vector_ref(api::context& c, ast_manager & m): api::object(c), m_ast_vector(m) {}
     virtual ~Z3_ast_vector_ref() {}
 };
 
diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index ceccff939..43c95ecdd 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -32,6 +32,28 @@ void install_tactics(tactic_manager & ctx);
 
 namespace api {
 
+    object::object(context& c): m_ref_count(0), m_context(c) { this->m_id = m_context.add_object(this); }
+
+    void object::inc_ref() { m_ref_count++; }
+
+    void object::dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) m_context.del_object(this); }
+    
+    unsigned context::add_object(api::object* o) {
+        unsigned id = m_allocated_objects.size();
+        if (!m_free_object_ids.empty()) {
+            id = m_free_object_ids.back();
+            m_free_object_ids.pop_back();
+        }
+        m_allocated_objects.insert(id, o);
+        return id;
+    }
+
+    void context::del_object(api::object* o) {
+        m_free_object_ids.push_back(o->id());
+        m_allocated_objects.remove(o->id());
+        dealloc(o);
+    }
+
     static void default_error_handler(Z3_context ctx, Z3_error_code c) {
         printf("Error: %s\n", Z3_get_error_msg(ctx, c));
         exit(1);
@@ -106,6 +128,14 @@ namespace api {
 
     context::~context() {
         reset_parser();
+        m_last_obj = 0;
+        u_map<api::object*>::iterator it = m_allocated_objects.begin();
+        while (it != m_allocated_objects.end()) {
+            //warning_msg("Junk: %d", it->m_key);
+            m_allocated_objects.remove(it->m_key);
+            dealloc(it->m_value);
+            it = m_allocated_objects.begin();
+        }
     }
 
     void context::interrupt() {
diff --git a/src/api/api_context.h b/src/api/api_context.h
index fa6754120..7cba15c44 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -35,6 +35,7 @@ Revision History:
 #include"tactic_manager.h"
 #include"context_params.h"
 #include"api_polynomial.h"
+#include"hashtable.h"
 
 namespace smtlib {
     class parser;
@@ -69,6 +70,8 @@ namespace api {
         ast_ref_vector             m_ast_trail;   //!< used when m_user_ref_count == false
 
         ref<api::object>           m_last_obj; //!< reference to the last API object returned by the APIs
+        u_map<api::object*>        m_allocated_objects; // !< table containing current set of allocated API objects
+        unsigned_vector            m_free_object_ids;   // !< free list of identifiers available for allocated objects.
 
         family_id                  m_basic_fid;
         family_id                  m_array_fid;
@@ -141,6 +144,9 @@ namespace api {
         // Sign an error if solver is searching
         void check_searching();
 
+        unsigned add_object(api::object* o);
+        void del_object(api::object* o);
+
         Z3_ast_print_mode get_print_mode() const { return m_print_mode; }
         void set_print_mode(Z3_ast_print_mode m) { m_print_mode = m; }
 
diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp
index be9f5894f..903fedd0f 100644
--- a/src/api/api_datalog.cpp
+++ b/src/api/api_datalog.cpp
@@ -223,7 +223,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_fixedpoint(c);
         RESET_ERROR_CODE();
-        Z3_fixedpoint_ref * d = alloc(Z3_fixedpoint_ref);
+        Z3_fixedpoint_ref * d = alloc(Z3_fixedpoint_ref, *mk_c(c));
         d->m_datalog = alloc(api::fixedpoint_context, mk_c(c)->m(), mk_c(c)->fparams());
         mk_c(c)->save_object(d);
         Z3_fixedpoint r = of_datalog(d);
@@ -369,7 +369,7 @@ extern "C" {
             return 0;
         }
 
-        Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
+        Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m);
         mk_c(c)->save_object(v);
         for (unsigned i = 0; i < coll.m_queries.size(); ++i) {
             v->m_ast_vector.push_back(coll.m_queries[i].get());
@@ -421,7 +421,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_fixedpoint_get_statistics(c, d);
         RESET_ERROR_CODE();
-        Z3_stats_ref * st = alloc(Z3_stats_ref);
+        Z3_stats_ref * st = alloc(Z3_stats_ref, (*mk_c(c)));
         to_fixedpoint_ref(d)->ctx().collect_statistics(st->m_stats);
         mk_c(c)->save_object(st);
         Z3_stats r = of_stats(st);
@@ -460,7 +460,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_fixedpoint_get_rules(c, d);
         ast_manager& m = mk_c(c)->m();
-        Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
+        Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m);
         mk_c(c)->save_object(v);
         expr_ref_vector rules(m), queries(m);
         svector<symbol> names;
@@ -483,7 +483,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_fixedpoint_get_assertions(c, d);
         ast_manager& m = mk_c(c)->m();
-        Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
+        Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m);
         mk_c(c)->save_object(v);
         unsigned num_asserts = to_fixedpoint_ref(d)->ctx().get_num_assertions();
         for (unsigned i = 0; i < num_asserts; ++i) {
@@ -568,7 +568,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_fixedpoint_get_param_descrs(c, f);
         RESET_ERROR_CODE();
-        Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref);
+        Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c));
         mk_c(c)->save_object(d);
         to_fixedpoint_ref(f)->collect_param_descrs(d->m_descrs);
         Z3_param_descrs r = of_param_descrs(d);
diff --git a/src/api/api_datalog.h b/src/api/api_datalog.h
index 8317426c1..8c095d546 100644
--- a/src/api/api_datalog.h
+++ b/src/api/api_datalog.h
@@ -30,13 +30,14 @@ typedef void (*reduce_assign_callback_fptr)(void*, func_decl*, unsigned, expr*co
 
 namespace api {
     class fixedpoint_context;
+    class context;
 };
 
 
 struct Z3_fixedpoint_ref : public api::object {
     api::fixedpoint_context *   m_datalog;
     params_ref               m_params;
-    Z3_fixedpoint_ref():m_datalog(0) {}
+    Z3_fixedpoint_ref(api::context& c): api::object(c), m_datalog(0) {}
     virtual ~Z3_fixedpoint_ref() { dealloc(m_datalog); }
 };
 
diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp
index 10164f5b9..ed4816e09 100644
--- a/src/api/api_goal.cpp
+++ b/src/api/api_goal.cpp
@@ -32,7 +32,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
-        Z3_goal_ref * g = alloc(Z3_goal_ref);
+        Z3_goal_ref * g = alloc(Z3_goal_ref, *mk_c(c));
         g->m_goal       = alloc(goal, mk_c(c)->m(), proofs != 0, models != 0, unsat_cores != 0);
         mk_c(c)->save_object(g);
         Z3_goal r       = of_goal(g);
@@ -156,7 +156,7 @@ extern "C" {
         LOG_Z3_goal_translate(c, g, target);
         RESET_ERROR_CODE();
         ast_translation translator(mk_c(c)->m(), mk_c(target)->m());
-        Z3_goal_ref * _r = alloc(Z3_goal_ref);
+        Z3_goal_ref * _r = alloc(Z3_goal_ref, *mk_c(c));
         _r->m_goal       = to_goal_ref(g)->translate(translator);
         mk_c(target)->save_object(_r);
         Z3_goal r = of_goal(_r);
diff --git a/src/api/api_goal.h b/src/api/api_goal.h
index c3d4d44f2..1e47b832a 100644
--- a/src/api/api_goal.h
+++ b/src/api/api_goal.h
@@ -23,6 +23,7 @@ Revision History:
 
 struct Z3_goal_ref : public api::object {
     goal_ref m_goal;
+    Z3_goal_ref(api::context& c) : api::object(c) {}
     virtual ~Z3_goal_ref() {}
 };
 
diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp
index 1e201c5b3..b14f3db72 100644
--- a/src/api/api_interp.cpp
+++ b/src/api/api_interp.cpp
@@ -212,7 +212,7 @@ extern "C" {
         LOG_Z3_get_interpolant(c, pf, pat, p);
         RESET_ERROR_CODE();
 
-        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
         mk_c(c)->save_object(v);
 
         ast *_pf = to_ast(pf);
@@ -303,7 +303,7 @@ extern "C" {
 
         if (_status == l_false){
             // copy result back
-            v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
+            v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
             mk_c(c)->save_object(v);
             for (unsigned i = 0; i < interp.size(); i++){
                 v->m_ast_vector.push_back(interp[i]);
@@ -314,7 +314,7 @@ extern "C" {
             model_ref mr;
             m_solver.get()->get_model(mr);
             if(mr.get()){
-                Z3_model_ref *tmp_val = alloc(Z3_model_ref);
+                Z3_model_ref *tmp_val = alloc(Z3_model_ref, *mk_c(c));
                 tmp_val->m_model = mr.get();
                 mk_c(c)->save_object(tmp_val);
                 *model = of_model(tmp_val);
diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index 10ede0922..67c0f2f08 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -86,7 +86,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             RETURN_Z3(0);
         }
-        Z3_func_interp_ref * fi = alloc(Z3_func_interp_ref, to_model_ref(m));
+        Z3_func_interp_ref * fi = alloc(Z3_func_interp_ref, *mk_c(c), to_model_ref(m));
         fi->m_func_interp       = _fi;
         mk_c(c)->save_object(fi);
         RETURN_Z3(of_func_interp(fi));
@@ -192,7 +192,7 @@ extern "C" {
             RETURN_Z3(0);
         }
         ptr_vector<expr> const & universe = to_model_ref(m)->get_universe(to_sort(s));
-        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
         mk_c(c)->save_object(v);
         unsigned sz = universe.size();
         for (unsigned i = 0; i < sz; i++) {
@@ -262,7 +262,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_IOB);
             RETURN_Z3(0);
         }
-        Z3_func_entry_ref * e = alloc(Z3_func_entry_ref, to_func_interp(f)->m_model.get());
+        Z3_func_entry_ref * e = alloc(Z3_func_entry_ref, *mk_c(c), to_func_interp(f)->m_model.get());
         e->m_func_interp = to_func_interp_ref(f);
         e->m_func_entry  = to_func_interp_ref(f)->get_entry(i);
         mk_c(c)->save_object(e);
diff --git a/src/api/api_model.h b/src/api/api_model.h
index 719326aaf..9a53b59bc 100644
--- a/src/api/api_model.h
+++ b/src/api/api_model.h
@@ -23,7 +23,7 @@ Revision History:
 
 struct Z3_model_ref : public api::object {
     model_ref  m_model;
-    Z3_model_ref() {}
+    Z3_model_ref(api::context& c): api::object(c) {}
     virtual ~Z3_model_ref() {}
 };
 
@@ -34,7 +34,7 @@ inline model * to_model_ref(Z3_model s) { return to_model(s)->m_model.get(); }
 struct Z3_func_interp_ref : public api::object {
     model_ref     m_model; // must have it to prevent reference to m_func_interp to be killed.
     func_interp * m_func_interp;
-    Z3_func_interp_ref(model * m):m_model(m), m_func_interp(0) {}
+    Z3_func_interp_ref(api::context& c, model * m): api::object(c), m_model(m), m_func_interp(0) {}
     virtual ~Z3_func_interp_ref() {}
 };
 
@@ -46,7 +46,7 @@ struct Z3_func_entry_ref : public api::object {
     model_ref           m_model; // must have it to prevent reference to m_func_entry to be killed.
     func_interp *       m_func_interp;
     func_entry const *  m_func_entry;
-    Z3_func_entry_ref(model * m):m_model(m), m_func_interp(0), m_func_entry(0) {}
+    Z3_func_entry_ref(api::context& c, model * m):api::object(c), m_model(m), m_func_interp(0), m_func_entry(0) {}
     virtual ~Z3_func_entry_ref() {}
 };
 
diff --git a/src/api/api_opt.cpp b/src/api/api_opt.cpp
index 87510293f..c0a311929 100644
--- a/src/api/api_opt.cpp
+++ b/src/api/api_opt.cpp
@@ -31,7 +31,7 @@ extern "C" {
 
     struct Z3_optimize_ref : public api::object {
         opt::context* m_opt;
-        Z3_optimize_ref():m_opt(0) {}
+        Z3_optimize_ref(api::context& c): api::object(c), m_opt(0) {}
         virtual ~Z3_optimize_ref() { dealloc(m_opt); }
     };
     inline Z3_optimize_ref * to_optimize(Z3_optimize o) { return reinterpret_cast<Z3_optimize_ref *>(o); }
@@ -42,7 +42,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_optimize(c);
         RESET_ERROR_CODE();
-        Z3_optimize_ref * o = alloc(Z3_optimize_ref);
+        Z3_optimize_ref * o = alloc(Z3_optimize_ref, *mk_c(c));
         o->m_opt = alloc(opt::context,mk_c(c)->m());
         mk_c(c)->save_object(o);
         RETURN_Z3(of_optimize(o));
@@ -158,7 +158,7 @@ extern "C" {
         RESET_ERROR_CODE();
         model_ref _m;
         to_optimize_ptr(o)->get_model(_m);
-        Z3_model_ref * m_ref = alloc(Z3_model_ref); 
+        Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); 
         if (_m) {
             m_ref->m_model = _m;
         }
@@ -186,7 +186,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_optimize_get_param_descrs(c, o);
         RESET_ERROR_CODE();
-        Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref);
+        Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c));
         mk_c(c)->save_object(d);
         to_optimize_ptr(o)->collect_param_descrs(d->m_descrs);
         Z3_param_descrs r = of_param_descrs(d);
@@ -240,7 +240,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_optimize_get_statistics(c, d);
         RESET_ERROR_CODE();
-        Z3_stats_ref * st = alloc(Z3_stats_ref);
+        Z3_stats_ref * st = alloc(Z3_stats_ref, *mk_c(c));
         to_optimize_ptr(d)->collect_statistics(st->m_stats);
         mk_c(c)->save_object(st);
         Z3_stats r = of_stats(st);
diff --git a/src/api/api_params.cpp b/src/api/api_params.cpp
index f2dab4d77..1efaffca8 100644
--- a/src/api/api_params.cpp
+++ b/src/api/api_params.cpp
@@ -30,7 +30,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_params(c);
         RESET_ERROR_CODE();
-        Z3_params_ref * p = alloc(Z3_params_ref);
+        Z3_params_ref * p = alloc(Z3_params_ref, *mk_c(c));
         mk_c(c)->save_object(p);
         Z3_params r = of_params(p);
         RETURN_Z3(r);
diff --git a/src/api/api_polynomial.cpp b/src/api/api_polynomial.cpp
index c68427960..979d2ea50 100644
--- a/src/api/api_polynomial.cpp
+++ b/src/api/api_polynomial.cpp
@@ -53,7 +53,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;
         }
-        Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, mk_c(c)->m());
+        Z3_ast_vector_ref* result = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
         mk_c(c)->save_object(result);
         if (converter.is_var(to_expr(x))) {
             expr2var const & mapping = converter.get_mapping();
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index be03e5daf..06bba37fc 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -58,7 +58,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_simple_solver(c);
         RESET_ERROR_CODE();
-        Z3_solver_ref * s = alloc(Z3_solver_ref, mk_smt_solver_factory());
+        Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_smt_solver_factory());
         mk_c(c)->save_object(s);
         Z3_solver r = of_solver(s);
         RETURN_Z3(r);
@@ -69,7 +69,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_solver(c);
         RESET_ERROR_CODE();
-        Z3_solver_ref * s = alloc(Z3_solver_ref, mk_smt_strategic_solver_factory());
+        Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_smt_strategic_solver_factory());
         mk_c(c)->save_object(s);
         Z3_solver r = of_solver(s);
         RETURN_Z3(r);
@@ -80,7 +80,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_solver_for_logic(c, logic);
         RESET_ERROR_CODE();
-        Z3_solver_ref * s = alloc(Z3_solver_ref, mk_smt_strategic_solver_factory(to_symbol(logic)));
+        Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_smt_strategic_solver_factory(to_symbol(logic)));
         mk_c(c)->save_object(s);
         Z3_solver r = of_solver(s);
         RETURN_Z3(r);
@@ -91,7 +91,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_mk_solver_from_tactic(c, t);
         RESET_ERROR_CODE();
-        Z3_solver_ref * s = alloc(Z3_solver_ref, mk_tactic2solver_factory(to_tactic_ref(t)));
+        Z3_solver_ref * s = alloc(Z3_solver_ref, *mk_c(c), mk_tactic2solver_factory(to_tactic_ref(t)));
         mk_c(c)->save_object(s);
         Z3_solver r = of_solver(s);
         RETURN_Z3(r);
@@ -103,7 +103,7 @@ extern "C" {
         LOG_Z3_solver_translate(c, s, target);
         RESET_ERROR_CODE();
         params_ref const& p = to_solver(s)->m_params; 
-        Z3_solver_ref * sr = alloc(Z3_solver_ref, 0);
+        Z3_solver_ref * sr = alloc(Z3_solver_ref, *mk_c(c), 0);
         init_solver(c, s);
         sr->m_solver = to_solver(s)->m_solver->translate(mk_c(target)->m(), p);
         mk_c(target)->save_object(sr);
@@ -134,7 +134,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_solver_get_param_descrs(c, s);
         RESET_ERROR_CODE();
-        Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref);
+        Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c));
         mk_c(c)->save_object(d);
         bool initialized = to_solver(s)->m_solver.get() != 0;
         if (!initialized)
@@ -255,7 +255,7 @@ extern "C" {
         LOG_Z3_solver_get_assertions(c, s);
         RESET_ERROR_CODE();
         init_solver(c, s);
-        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
         mk_c(c)->save_object(v);
         unsigned sz = to_solver_ref(s)->get_num_assertions();
         for (unsigned i = 0; i < sz; i++) {
@@ -323,7 +323,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_USAGE);
             RETURN_Z3(0);
         }
-        Z3_model_ref * m_ref = alloc(Z3_model_ref); 
+        Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); 
         m_ref->m_model = _m;
         mk_c(c)->save_object(m_ref);
         RETURN_Z3(of_model(m_ref));
@@ -352,7 +352,7 @@ extern "C" {
         init_solver(c, s);
         ptr_vector<expr> core;
         to_solver_ref(s)->get_unsat_core(core);
-        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
         mk_c(c)->save_object(v);
         for (unsigned i = 0; i < core.size(); i++) {
             v->m_ast_vector.push_back(core[i]);
@@ -375,7 +375,7 @@ extern "C" {
         LOG_Z3_solver_get_statistics(c, s);
         RESET_ERROR_CODE();
         init_solver(c, s);
-        Z3_stats_ref * st = alloc(Z3_stats_ref);
+        Z3_stats_ref * st = alloc(Z3_stats_ref, *mk_c(c));
         to_solver_ref(s)->collect_statistics(st->m_stats);
         get_memory_statistics(st->m_stats);
         get_rlimit_statistics(mk_c(c)->m().limit(), st->m_stats);
diff --git a/src/api/api_solver.h b/src/api/api_solver.h
index 5ed7a15f7..ea59ccf33 100644
--- a/src/api/api_solver.h
+++ b/src/api/api_solver.h
@@ -26,7 +26,7 @@ struct Z3_solver_ref : public api::object {
     ref<solver>                m_solver;
     params_ref                 m_params;
     symbol                     m_logic;
-    Z3_solver_ref(solver_factory * f):m_solver_factory(f), m_solver(0), m_logic(symbol::null) {}
+    Z3_solver_ref(api::context& c, solver_factory * f): api::object(c), m_solver_factory(f), m_solver(0), m_logic(symbol::null) {}
     virtual ~Z3_solver_ref() {}
 };
 
diff --git a/src/api/api_stats.h b/src/api/api_stats.h
index e0e370336..1c0c0c82e 100644
--- a/src/api/api_stats.h
+++ b/src/api/api_stats.h
@@ -23,6 +23,7 @@ Revision History:
 
 struct Z3_stats_ref : public api::object {
     statistics m_stats;
+    Z3_stats_ref(api::context& c): api::object(c) {}
     virtual ~Z3_stats_ref() {}
 };
 
diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp
index 78e042528..7068619c1 100644
--- a/src/api/api_tactic.cpp
+++ b/src/api/api_tactic.cpp
@@ -25,13 +25,13 @@ Revision History:
 #include"cancel_eh.h"
 #include"scoped_timer.h"
 
-Z3_apply_result_ref::Z3_apply_result_ref(ast_manager & m):m_core(m) {
+Z3_apply_result_ref::Z3_apply_result_ref(api::context& c, ast_manager & m): api::object(c), m_core(m) {
 }
 
 extern "C" {
 
 #define RETURN_TACTIC(_t_) {                            \
-    Z3_tactic_ref * _ref_ = alloc(Z3_tactic_ref);       \
+        Z3_tactic_ref * _ref_ = alloc(Z3_tactic_ref, *mk_c(c)); \
     _ref_->m_tactic   = _t_;                            \
     mk_c(c)->save_object(_ref_);                        \
     Z3_tactic _result_  = of_tactic(_ref_);             \
@@ -39,7 +39,7 @@ extern "C" {
 }
 
 #define RETURN_PROBE(_t_) {                     \
-    Z3_probe_ref * _ref_ = alloc(Z3_probe_ref); \
+        Z3_probe_ref * _ref_ = alloc(Z3_probe_ref, *mk_c(c));   \
     _ref_->m_probe   = _t_;                     \
     mk_c(c)->save_object(_ref_);                \
     Z3_probe _result_  = of_probe(_ref_);       \
@@ -367,7 +367,7 @@ extern "C" {
         Z3_TRY;
         LOG_Z3_tactic_get_param_descrs(c, t);
         RESET_ERROR_CODE();
-        Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref);
+        Z3_param_descrs_ref * d = alloc(Z3_param_descrs_ref, *mk_c(c));
         mk_c(c)->save_object(d);
         to_tactic_ref(t)->collect_param_descrs(d->m_descrs);
         Z3_param_descrs r = of_param_descrs(d);
@@ -404,7 +404,7 @@ extern "C" {
     static Z3_apply_result _tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g, params_ref p) {
         goal_ref new_goal;
         new_goal = alloc(goal, *to_goal_ref(g));
-        Z3_apply_result_ref * ref = alloc(Z3_apply_result_ref, mk_c(c)->m());
+        Z3_apply_result_ref * ref = alloc(Z3_apply_result_ref, (*mk_c(c)), mk_c(c)->m());
         mk_c(c)->save_object(ref); 
 
         unsigned timeout     = p.get_uint("timeout", UINT_MAX);
@@ -505,7 +505,7 @@ extern "C" {
             SET_ERROR_CODE(Z3_IOB);
             RETURN_Z3(0);
         }
-        Z3_goal_ref * g = alloc(Z3_goal_ref);
+        Z3_goal_ref * g = alloc(Z3_goal_ref, *mk_c(c));
         g->m_goal       = to_apply_result(r)->m_subgoals[i];
         mk_c(c)->save_object(g);
         Z3_goal result  = of_goal(g);
@@ -524,7 +524,7 @@ extern "C" {
         model_ref new_m = to_model_ref(m)->copy();
         if (to_apply_result(r)->m_mc)
             to_apply_result(r)->m_mc->operator()(new_m, i);
-        Z3_model_ref * m_ref = alloc(Z3_model_ref); 
+        Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); 
         m_ref->m_model = new_m;
         mk_c(c)->save_object(m_ref);
         RETURN_Z3(of_model(m_ref));
diff --git a/src/api/api_tactic.h b/src/api/api_tactic.h
index 6f8d83fd9..373b85b39 100644
--- a/src/api/api_tactic.h
+++ b/src/api/api_tactic.h
@@ -21,13 +21,20 @@ Revision History:
 #include"api_goal.h"
 #include"tactical.h"
 
+namespace api {
+    class context;
+}
+
+
 struct Z3_tactic_ref : public api::object {
     tactic_ref   m_tactic;
+    Z3_tactic_ref(api::context& c): api::object(c) {}
     virtual ~Z3_tactic_ref() {}
 };
 
 struct Z3_probe_ref : public api::object {
     probe_ref    m_probe;
+    Z3_probe_ref(api::context& c):api::object(c) {}
     virtual ~Z3_probe_ref() {}
 };
 
@@ -44,7 +51,7 @@ struct Z3_apply_result_ref : public api::object {
     model_converter_ref  m_mc;
     proof_converter_ref  m_pc;
     expr_dependency_ref  m_core;
-    Z3_apply_result_ref(ast_manager & m);
+    Z3_apply_result_ref(api::context& c, ast_manager & m);
     virtual ~Z3_apply_result_ref() {}
 };
 
diff --git a/src/api/api_util.h b/src/api/api_util.h
index 3b7baeac0..7857e7c38 100644
--- a/src/api/api_util.h
+++ b/src/api/api_util.h
@@ -31,15 +31,20 @@ Revision History:
 #define CHECK_REF_COUNT(a) (reinterpret_cast<ast const*>(a)->get_ref_count() > 0)
 
 namespace api {
+    class context;
+
     // Generic wrapper for ref-count objects exposed by the API
     class object {
         unsigned m_ref_count;
+        unsigned m_id;
+        context& m_context;
     public:
-        object():m_ref_count(0) {}
+        object(context& c);
         virtual ~object() {}
         unsigned ref_count() const { return m_ref_count; }
-        void inc_ref() { m_ref_count++; }
-        void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); }
+        unsigned id() const { return m_id; }
+        void inc_ref();
+        void dec_ref();
     };
 };
 
@@ -82,6 +87,7 @@ inline lbool    to_lbool(Z3_lbool b) { return static_cast<lbool>(b); }
 
 struct Z3_params_ref : public api::object {
     params_ref m_params;
+    Z3_params_ref(api::context& c): api::object(c) {}
     virtual ~Z3_params_ref() {}
 };
 
@@ -91,6 +97,7 @@ inline params_ref to_param_ref(Z3_params p) { return p == 0 ? params_ref() : to_
 
 struct Z3_param_descrs_ref : public api::object {
     param_descrs m_descrs;
+    Z3_param_descrs_ref(api::context& c): api::object(c) {}
     virtual ~Z3_param_descrs_ref() {}
 };
 
diff --git a/src/util/hashtable.h b/src/util/hashtable.h
index fbf36242b..ddf40f39f 100644
--- a/src/util/hashtable.h
+++ b/src/util/hashtable.h
@@ -645,7 +645,6 @@ public:
     ptr_addr_hashtable(unsigned initial_capacity = DEFAULT_HASHTABLE_INITIAL_CAPACITY):
         core_hashtable<ptr_addr_hash_entry<T>, ptr_hash<T>, ptr_eq<T> >(initial_capacity) {}
 
-    // Using iterators to traverse the elements of this kind of hashtable will produce non-determinism.
     iterator begin() const { 
         UNREACHABLE();
     }
@@ -653,6 +652,9 @@ public:
     iterator end() const { 
         UNREACHABLE();
     }
+
+    // NB. Using iterators to traverse the elements of this kind of hashtable will produce non-determinism.
+
 };
 
 /**