diff --git a/src/api/dotnet/AST.cs b/src/api/dotnet/AST.cs
index 0afff2c42..48a7175eb 100644
--- a/src/api/dotnet/AST.cs
+++ b/src/api/dotnet/AST.cs
@@ -208,37 +208,22 @@ namespace Microsoft.Z3
         internal AST(Context ctx) : base(ctx) { Debug.Assert(ctx != null); }
         internal AST(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            // Console.WriteLine("AST IncRef()");
-            if (Context == null || o == IntPtr.Zero)
-                return;
-            Context.AST_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            if (Context != null && o != IntPtr.Zero)
+                Native.Z3_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            // Console.WriteLine("AST DecRef()");
-            if (Context == null || o == IntPtr.Zero)
-                return;
-            Context.AST_DRQ.Add(o);
-            base.DecRef(o);
+            if (Context != null && o != IntPtr.Zero)
+            {
+                lock (Context)
+                {
+                    if (Context.nCtx != IntPtr.Zero)
+                        Native.Z3_dec_ref(Context.nCtx, o);
+                }
+            }
         }
 
         internal static AST Create(Context ctx, IntPtr obj)
diff --git a/src/api/dotnet/ASTMap.cs b/src/api/dotnet/ASTMap.cs
index 0dde04411..ad3c47106 100644
--- a/src/api/dotnet/ASTMap.cs
+++ b/src/api/dotnet/ASTMap.cs
@@ -125,31 +125,18 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_ast_map_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_ast_map_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.ASTMap_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_ast_map_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.ASTMap_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_ast_map_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }
diff --git a/src/api/dotnet/ASTVector.cs b/src/api/dotnet/ASTVector.cs
index fcfa6bd65..777d7d56c 100644
--- a/src/api/dotnet/ASTVector.cs
+++ b/src/api/dotnet/ASTVector.cs
@@ -233,31 +233,19 @@ namespace Microsoft.Z3
         internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
         internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Debug.Assert(ctx != null); }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_ast_vector_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_ast_vector_dec_ref(ctx.nCtx, obj);
-            }
-        };
 
         internal override void IncRef(IntPtr o)
         {
-            Context.ASTVector_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_ast_vector_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.ASTVector_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_ast_vector_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }
diff --git a/src/api/dotnet/ApplyResult.cs b/src/api/dotnet/ApplyResult.cs
index 342bf3216..728fde3d5 100644
--- a/src/api/dotnet/ApplyResult.cs
+++ b/src/api/dotnet/ApplyResult.cs
@@ -67,31 +67,18 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_apply_result_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_apply_result_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.ApplyResult_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_apply_result_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.ApplyResult_DRQ.Add(o);
-            base.DecRef(o);
+            lock(Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_apply_result_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index af982b2d4..5aabcbc39 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -75,6 +75,7 @@ namespace Microsoft.Z3
                 foreach (KeyValuePair<string, string> kv in settings)
                     Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
                 m_ctx = Native.Z3_mk_context_rc(cfg);
+                Native.Z3_enable_concurrent_dec_ref(m_ctx);
                 Native.Z3_del_config(cfg);
                 InitContext();
             }
@@ -4852,123 +4853,9 @@ namespace Microsoft.Z3
 
         private void ObjectInvariant()
         {
-            Debug.Assert(m_AST_DRQ != null);
-            Debug.Assert(m_ASTMap_DRQ != null);
-            Debug.Assert(m_ASTVector_DRQ != null);
-            Debug.Assert(m_ApplyResult_DRQ != null);
-            Debug.Assert(m_FuncEntry_DRQ != null);
-            Debug.Assert(m_FuncInterp_DRQ != null);
-            Debug.Assert(m_Goal_DRQ != null);
-            Debug.Assert(m_Model_DRQ != null);
-            Debug.Assert(m_Params_DRQ != null);
-            Debug.Assert(m_ParamDescrs_DRQ != null);
-            Debug.Assert(m_Probe_DRQ != null);
-            Debug.Assert(m_Solver_DRQ != null);
-            Debug.Assert(m_Statistics_DRQ != null);
-            Debug.Assert(m_Tactic_DRQ != null);
-            Debug.Assert(m_Fixedpoint_DRQ != null);
-            Debug.Assert(m_Optimize_DRQ != null);
+            // none
         }
 
-        readonly private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue();
-        readonly private ASTMap.DecRefQueue m_ASTMap_DRQ = new ASTMap.DecRefQueue(10);
-        readonly private ASTVector.DecRefQueue m_ASTVector_DRQ = new ASTVector.DecRefQueue(10);
-        readonly private ApplyResult.DecRefQueue m_ApplyResult_DRQ = new ApplyResult.DecRefQueue(10);
-        readonly private FuncInterp.Entry.DecRefQueue m_FuncEntry_DRQ = new FuncInterp.Entry.DecRefQueue(10);
-        readonly private FuncInterp.DecRefQueue m_FuncInterp_DRQ = new FuncInterp.DecRefQueue(10);
-        readonly private Goal.DecRefQueue m_Goal_DRQ = new Goal.DecRefQueue(10);
-        readonly private Model.DecRefQueue m_Model_DRQ = new Model.DecRefQueue(10);
-        readonly private Params.DecRefQueue m_Params_DRQ = new Params.DecRefQueue(10);
-        readonly private ParamDescrs.DecRefQueue m_ParamDescrs_DRQ = new ParamDescrs.DecRefQueue(10);
-        readonly private Probe.DecRefQueue m_Probe_DRQ = new Probe.DecRefQueue(10);
-        readonly private Solver.DecRefQueue m_Solver_DRQ = new Solver.DecRefQueue(10);
-        readonly private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue(10);
-        readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue(10);
-        readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue(10);
-        readonly private Optimize.DecRefQueue m_Optimize_DRQ = new Optimize.DecRefQueue(10);
-
-        /// <summary>
-        /// AST DRQ
-        /// </summary>
-        public IDecRefQueue AST_DRQ { get { return m_AST_DRQ; } }
-
-        /// <summary>
-        /// ASTMap DRQ
-        /// </summary>
-        public IDecRefQueue ASTMap_DRQ { get { return m_ASTMap_DRQ; } }
-
-        /// <summary>
-        /// ASTVector DRQ
-        /// </summary>
-        public IDecRefQueue ASTVector_DRQ { get { return m_ASTVector_DRQ; } }
-
-        /// <summary>
-        /// ApplyResult DRQ
-        /// </summary>
-        public IDecRefQueue ApplyResult_DRQ { get { return m_ApplyResult_DRQ; } }
-
-        /// <summary>
-        /// FuncEntry DRQ
-        /// </summary>
-        public IDecRefQueue FuncEntry_DRQ { get { return m_FuncEntry_DRQ; } }
-
-        /// <summary>
-        /// FuncInterp DRQ
-        /// </summary>
-        public IDecRefQueue FuncInterp_DRQ { get { return m_FuncInterp_DRQ; } }
-
-        /// <summary>
-        /// Goal DRQ
-        /// </summary>
-        public IDecRefQueue Goal_DRQ { get { return m_Goal_DRQ; } }
-
-        /// <summary>
-        /// Model DRQ
-        /// </summary>
-        public IDecRefQueue Model_DRQ { get { return m_Model_DRQ; } }
-
-        /// <summary>
-        /// Params DRQ
-        /// </summary>
-        public IDecRefQueue Params_DRQ { get { return m_Params_DRQ; } }
-
-        /// <summary>
-        /// ParamDescrs DRQ
-        /// </summary>
-        public IDecRefQueue ParamDescrs_DRQ { get { return m_ParamDescrs_DRQ; } }
-
-        /// <summary>
-        /// Probe DRQ
-        /// </summary>
-        public IDecRefQueue Probe_DRQ { get { return m_Probe_DRQ; } }
-
-        /// <summary>
-        /// Solver DRQ
-        /// </summary>
-        public IDecRefQueue Solver_DRQ { get { return m_Solver_DRQ; } }
-
-        /// <summary>
-        /// Statistics DRQ
-        /// </summary>
-        public IDecRefQueue Statistics_DRQ { get { return m_Statistics_DRQ; } }
-
-        /// <summary>
-        /// Tactic DRQ
-        /// </summary>
-        public IDecRefQueue Tactic_DRQ { get { return m_Tactic_DRQ; } }
-
-        /// <summary>
-        /// FixedPoint DRQ
-        /// </summary>
-        public IDecRefQueue Fixedpoint_DRQ { get { return m_Fixedpoint_DRQ; } }
-
-        /// <summary>
-        /// Optimize DRQ
-        /// </summary>
-        public IDecRefQueue Optimize_DRQ { get { return m_Fixedpoint_DRQ; } }
-
-        internal long refCount = 0;
-
         /// <summary>
         /// Finalizer.
         /// </summary>
@@ -4984,22 +4871,6 @@ namespace Microsoft.Z3
         public void Dispose()
         {
             // Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
-            AST_DRQ.Clear(this);
-            ASTMap_DRQ.Clear(this);
-            ASTVector_DRQ.Clear(this);
-            ApplyResult_DRQ.Clear(this);
-            FuncEntry_DRQ.Clear(this);
-            FuncInterp_DRQ.Clear(this);
-            Goal_DRQ.Clear(this);
-            Model_DRQ.Clear(this);
-            Params_DRQ.Clear(this);
-            ParamDescrs_DRQ.Clear(this);
-            Probe_DRQ.Clear(this);
-            Solver_DRQ.Clear(this);
-            Statistics_DRQ.Clear(this);
-            Tactic_DRQ.Clear(this);
-            Fixedpoint_DRQ.Clear(this);
-            Optimize_DRQ.Clear(this);
 
             if (m_boolSort != null) m_boolSort.Dispose();
             if (m_intSort != null) m_intSort.Dispose();
@@ -5011,13 +4882,16 @@ namespace Microsoft.Z3
             m_realSort = null;
             m_stringSort = null;
             m_charSort = null;
-            if (refCount == 0 && m_ctx != IntPtr.Zero)
+            if (m_ctx != IntPtr.Zero)
             {
-                m_n_err_handler = null;
                 IntPtr ctx = m_ctx;
-                m_ctx = IntPtr.Zero;
-                if (!is_external) 
-                   Native.Z3_del_context(ctx);
+                lock (this)
+                {
+                    m_n_err_handler = null;
+                    m_ctx = IntPtr.Zero;
+                }
+                if (!is_external)
+                    Native.Z3_del_context(ctx);
             }
             else
                 GC.ReRegisterForFinalize(this);
diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs
index 15560d829..2edae1e2a 100644
--- a/src/api/dotnet/Fixedpoint.cs
+++ b/src/api/dotnet/Fixedpoint.cs
@@ -318,31 +318,18 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_fixedpoint_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_fixedpoint_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.Fixedpoint_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_fixedpoint_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Fixedpoint_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_fixedpoint_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }
diff --git a/src/api/dotnet/FuncInterp.cs b/src/api/dotnet/FuncInterp.cs
index 6924049d3..fec6eab95 100644
--- a/src/api/dotnet/FuncInterp.cs
+++ b/src/api/dotnet/FuncInterp.cs
@@ -85,31 +85,18 @@ namespace Microsoft.Z3
             #region Internal
             internal Entry(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
 
-            internal class DecRefQueue : IDecRefQueue
-            {
-                public DecRefQueue() : base() { }
-                public DecRefQueue(uint move_limit) : base(move_limit) { }
-                internal override void IncRef(Context ctx, IntPtr obj)
-                {
-                    Native.Z3_func_entry_inc_ref(ctx.nCtx, obj);
-                }
-
-                internal override void DecRef(Context ctx, IntPtr obj)
-                {
-                    Native.Z3_func_entry_dec_ref(ctx.nCtx, obj);
-                }
-            };
-
             internal override void IncRef(IntPtr o)
             {
-                Context.FuncEntry_DRQ.IncAndClear(Context, o);
-                base.IncRef(o);
+                Native.Z3_func_entry_inc_ref(Context.nCtx, o);
             }
 
             internal override void DecRef(IntPtr o)
             {
-                Context.FuncEntry_DRQ.Add(o);
-                base.DecRef(o);
+                lock (Context)
+                {
+                    if (Context.nCtx != IntPtr.Zero)
+                        Native.Z3_func_entry_dec_ref(Context.nCtx, o);
+                }
             }
             #endregion
         };
@@ -190,31 +177,18 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_func_interp_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_func_interp_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.FuncInterp_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_func_interp_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.FuncInterp_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_func_interp_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }
diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs
index c096c0755..8183c7a79 100644
--- a/src/api/dotnet/Goal.cs
+++ b/src/api/dotnet/Goal.cs
@@ -252,33 +252,20 @@ namespace Microsoft.Z3
             : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (byte)(models ? 1 : 0), (byte)(unsatCores ? 1 : 0), (byte)(proofs ? 1 : 0)))
         {
             Debug.Assert(ctx != null);
-        }
-
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_goal_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_goal_dec_ref(ctx.nCtx, obj);
-            }
-        };        
+        }      
 
         internal override void IncRef(IntPtr o)
         {
-            Context.Goal_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_goal_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Goal_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_goal_dec_ref(Context.nCtx, o);
+            }
         }
 
         #endregion
diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs
index c35c0a727..343b2beee 100644
--- a/src/api/dotnet/Model.cs
+++ b/src/api/dotnet/Model.cs
@@ -302,33 +302,20 @@ namespace Microsoft.Z3
             : base(ctx, obj)
         {
             Debug.Assert(ctx != null);
-        }
-
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_model_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_model_dec_ref(ctx.nCtx, obj);
-            }
-        };        
+        }      
 
         internal override void IncRef(IntPtr o)
         {
-            Context.Model_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_model_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Model_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_model_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }
diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs
index ecd5e8e82..0694faabe 100644
--- a/src/api/dotnet/Optimize.cs
+++ b/src/api/dotnet/Optimize.cs
@@ -440,31 +440,18 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_optimize_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_optimize_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.Optimize_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_optimize_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Optimize_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_optimize_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }
diff --git a/src/api/dotnet/ParamDescrs.cs b/src/api/dotnet/ParamDescrs.cs
index fbfb9cd16..1975037e3 100644
--- a/src/api/dotnet/ParamDescrs.cs
+++ b/src/api/dotnet/ParamDescrs.cs
@@ -91,33 +91,20 @@ namespace Microsoft.Z3
             : base(ctx, obj)
         {
             Debug.Assert(ctx != null);
-        }
-
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_param_descrs_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_param_descrs_dec_ref(ctx.nCtx, obj);
-            }
-        };        
+        }       
 
         internal override void IncRef(IntPtr o)
         {
-            Context.ParamDescrs_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_param_descrs_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.ParamDescrs_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_param_descrs_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }
diff --git a/src/api/dotnet/Params.cs b/src/api/dotnet/Params.cs
index e5926934a..64dd34968 100644
--- a/src/api/dotnet/Params.cs
+++ b/src/api/dotnet/Params.cs
@@ -147,33 +147,20 @@ namespace Microsoft.Z3
             : base(ctx, Native.Z3_mk_params(ctx.nCtx))
         {
             Debug.Assert(ctx != null);
-        }
-
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_params_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_params_dec_ref(ctx.nCtx, obj);
-            }
-        };        
+        }      
 
         internal override void IncRef(IntPtr o)
         {
-            Context.Params_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_params_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Params_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_params_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }
diff --git a/src/api/dotnet/Probe.cs b/src/api/dotnet/Probe.cs
index 5cdee79a2..e0457c2fe 100644
--- a/src/api/dotnet/Probe.cs
+++ b/src/api/dotnet/Probe.cs
@@ -70,31 +70,18 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_probe_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_probe_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.Probe_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_probe_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Probe_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_probe_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }
diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs
index 52f2ad993..00b5117ea 100644
--- a/src/api/dotnet/Solver.cs
+++ b/src/api/dotnet/Solver.cs
@@ -538,31 +538,18 @@ namespace Microsoft.Z3
             this.BacktrackLevel = uint.MaxValue;
         }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_solver_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_solver_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.Solver_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_solver_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Solver_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_solver_dec_ref(Context.nCtx, o);
+            }
         }
 
         private Status lboolToStatus(Z3_lbool r) 
diff --git a/src/api/dotnet/Statistics.cs b/src/api/dotnet/Statistics.cs
index f6d72e0c7..1811951a2 100644
--- a/src/api/dotnet/Statistics.cs
+++ b/src/api/dotnet/Statistics.cs
@@ -19,8 +19,6 @@ Notes:
 
 using System;
 using System.Diagnostics;
-
-
 namespace Microsoft.Z3
 {
 
@@ -189,31 +187,18 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
 
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_stats_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_stats_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.Statistics_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_stats_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Statistics_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_stats_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }
diff --git a/src/api/dotnet/Tactic.cs b/src/api/dotnet/Tactic.cs
index 96b6da170..d87b8bc48 100644
--- a/src/api/dotnet/Tactic.cs
+++ b/src/api/dotnet/Tactic.cs
@@ -107,34 +107,18 @@ namespace Microsoft.Z3
             Debug.Assert(ctx != null);
         }
 
-        /// <summary>
-        /// DecRefQueue
-        /// </summary>
-        internal class DecRefQueue : IDecRefQueue
-        {
-            public DecRefQueue() : base() { }
-            public DecRefQueue(uint move_limit) : base(move_limit) { }
-            internal override void IncRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_tactic_inc_ref(ctx.nCtx, obj);
-            }
-
-            internal override void DecRef(Context ctx, IntPtr obj)
-            {
-                Native.Z3_tactic_dec_ref(ctx.nCtx, obj);
-            }
-        };
-
         internal override void IncRef(IntPtr o)
         {
-            Context.Tactic_DRQ.IncAndClear(Context, o);
-            base.IncRef(o);
+            Native.Z3_tactic_inc_ref(Context.nCtx, o);
         }
 
         internal override void DecRef(IntPtr o)
         {
-            Context.Tactic_DRQ.Add(o);
-            base.DecRef(o);
+            lock (Context)
+            {
+                if (Context.nCtx != IntPtr.Zero)
+                    Native.Z3_tactic_dec_ref(Context.nCtx, o);
+            }
         }
         #endregion
     }
diff --git a/src/api/dotnet/Z3Object.cs b/src/api/dotnet/Z3Object.cs
index 432885b66..1affa9d17 100644
--- a/src/api/dotnet/Z3Object.cs
+++ b/src/api/dotnet/Z3Object.cs
@@ -52,8 +52,6 @@ namespace Microsoft.Z3
 
             if (m_ctx != null)
             {
-                if (Interlocked.Decrement(ref m_ctx.refCount) == 0)
-                    GC.ReRegisterForFinalize(m_ctx);
                 m_ctx = null;
             }
 
@@ -76,16 +74,12 @@ namespace Microsoft.Z3
         internal Z3Object(Context ctx)
         {
             Debug.Assert(ctx != null);
-
-            Interlocked.Increment(ref ctx.refCount);
             m_ctx = ctx;
         }
 
         internal Z3Object(Context ctx, IntPtr obj)
         {
             Debug.Assert(ctx != null);
-
-            Interlocked.Increment(ref ctx.refCount);
             m_ctx = ctx;
             IncRef(obj);
             m_n_obj = obj;