diff --git a/src/api/dotnet/AST.cs b/src/api/dotnet/AST.cs
index 552fd6def..2ffaaa661 100644
--- a/src/api/dotnet/AST.cs
+++ b/src/api/dotnet/AST.cs
@@ -215,12 +215,12 @@ namespace Microsoft.Z3
         {
             public DecRefQueue() : base() { }
             public DecRefQueue(uint move_limit) : base(move_limit) { }
-            public override void IncRef(Context ctx, IntPtr obj)
+            internal override void IncRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_inc_ref(ctx.nCtx, obj);
             }
 
-            public override void DecRef(Context ctx, IntPtr obj)
+            internal override void DecRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_dec_ref(ctx.nCtx, obj);
             }
diff --git a/src/api/dotnet/ASTMap.cs b/src/api/dotnet/ASTMap.cs
index fa8070908..6f296147e 100644
--- a/src/api/dotnet/ASTMap.cs
+++ b/src/api/dotnet/ASTMap.cs
@@ -130,12 +130,12 @@ namespace Microsoft.Z3
         {
             public DecRefQueue() : base() { }
             public DecRefQueue(uint move_limit) : base(move_limit) { }
-            public override void IncRef(Context ctx, IntPtr obj)
+            internal override void IncRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_ast_map_inc_ref(ctx.nCtx, obj);
             }
 
-            public override void DecRef(Context ctx, IntPtr obj)
+            internal override void DecRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_ast_map_dec_ref(ctx.nCtx, obj);
             }
diff --git a/src/api/dotnet/ASTVector.cs b/src/api/dotnet/ASTVector.cs
index be5172f97..597b1decc 100644
--- a/src/api/dotnet/ASTVector.cs
+++ b/src/api/dotnet/ASTVector.cs
@@ -107,12 +107,12 @@ namespace Microsoft.Z3
         {
             public DecRefQueue() : base() { }
             public DecRefQueue(uint move_limit) : base(move_limit) { }
-            public override void IncRef(Context ctx, IntPtr obj)
+            internal override void IncRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_ast_vector_inc_ref(ctx.nCtx, obj);
             }
 
-            public override void DecRef(Context ctx, IntPtr obj)
+            internal override void DecRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_ast_vector_dec_ref(ctx.nCtx, obj);
             }
diff --git a/src/api/dotnet/ApplyResult.cs b/src/api/dotnet/ApplyResult.cs
index 4ff8851af..608be7080 100644
--- a/src/api/dotnet/ApplyResult.cs
+++ b/src/api/dotnet/ApplyResult.cs
@@ -87,12 +87,12 @@ namespace Microsoft.Z3
         {
             public DecRefQueue() : base() { }
             public DecRefQueue(uint move_limit) : base(move_limit) { }
-            public override void IncRef(Context ctx, IntPtr obj)
+            internal override void IncRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_apply_result_inc_ref(ctx.nCtx, obj);
             }
 
-            public override void DecRef(Context ctx, IntPtr obj)
+            internal override void DecRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_apply_result_dec_ref(ctx.nCtx, obj);
             }
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 3c3a960df..d14c591aa 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -4411,21 +4411,80 @@ namespace Microsoft.Z3
         readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue(10);
         readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue(10);
 
-        internal AST.DecRefQueue AST_DRQ { get { Contract.Ensures(Contract.Result<AST.DecRefQueue>() != null); return m_AST_DRQ; } }
-        internal ASTMap.DecRefQueue ASTMap_DRQ { get { Contract.Ensures(Contract.Result<ASTMap.DecRefQueue>() != null); return m_ASTMap_DRQ; } }
-        internal ASTVector.DecRefQueue ASTVector_DRQ { get { Contract.Ensures(Contract.Result<ASTVector.DecRefQueue>() != null); return m_ASTVector_DRQ; } }
-        internal ApplyResult.DecRefQueue ApplyResult_DRQ { get { Contract.Ensures(Contract.Result<ApplyResult.DecRefQueue>() != null); return m_ApplyResult_DRQ; } }
-        internal FuncInterp.Entry.DecRefQueue FuncEntry_DRQ { get { Contract.Ensures(Contract.Result<FuncInterp.Entry.DecRefQueue>() != null); return m_FuncEntry_DRQ; } }
-        internal FuncInterp.DecRefQueue FuncInterp_DRQ { get { Contract.Ensures(Contract.Result<FuncInterp.DecRefQueue>() != null); return m_FuncInterp_DRQ; } }
-        internal Goal.DecRefQueue Goal_DRQ { get { Contract.Ensures(Contract.Result<Goal.DecRefQueue>() != null); return m_Goal_DRQ; } }
-        internal Model.DecRefQueue Model_DRQ { get { Contract.Ensures(Contract.Result<Model.DecRefQueue>() != null); return m_Model_DRQ; } }
-        internal Params.DecRefQueue Params_DRQ { get { Contract.Ensures(Contract.Result<Params.DecRefQueue>() != null); return m_Params_DRQ; } }
-        internal ParamDescrs.DecRefQueue ParamDescrs_DRQ { get { Contract.Ensures(Contract.Result<ParamDescrs.DecRefQueue>() != null); return m_ParamDescrs_DRQ; } }
-        internal Probe.DecRefQueue Probe_DRQ { get { Contract.Ensures(Contract.Result<Probe.DecRefQueue>() != null); return m_Probe_DRQ; } }
-        internal Solver.DecRefQueue Solver_DRQ { get { Contract.Ensures(Contract.Result<Solver.DecRefQueue>() != null); return m_Solver_DRQ; } }
-        internal Statistics.DecRefQueue Statistics_DRQ { get { Contract.Ensures(Contract.Result<Statistics.DecRefQueue>() != null); return m_Statistics_DRQ; } }
-        internal Tactic.DecRefQueue Tactic_DRQ { get { Contract.Ensures(Contract.Result<Tactic.DecRefQueue>() != null); return m_Tactic_DRQ; } }
-        internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
+        /// <summary>
+        /// AST DRQ
+        /// </summary>
+        public IDecRefQueue AST_DRQ { get { Contract.Ensures(Contract.Result<AST.DecRefQueue>() != null); return m_AST_DRQ; } }
+
+        /// <summary>
+        /// ASTMap DRQ
+        /// </summary>
+        public IDecRefQueue ASTMap_DRQ { get { Contract.Ensures(Contract.Result<ASTMap.DecRefQueue>() != null); return m_ASTMap_DRQ; } }
+        
+        /// <summary>
+        /// ASTVector DRQ
+        /// </summary>
+        public IDecRefQueue ASTVector_DRQ { get { Contract.Ensures(Contract.Result<ASTVector.DecRefQueue>() != null); return m_ASTVector_DRQ; } }
+
+        /// <summary>
+        /// ApplyResult DRQ
+        /// </summary>
+        public IDecRefQueue ApplyResult_DRQ { get { Contract.Ensures(Contract.Result<ApplyResult.DecRefQueue>() != null); return m_ApplyResult_DRQ; } }
+
+        /// <summary>
+        /// FuncEntry DRQ
+        /// </summary>
+        public IDecRefQueue FuncEntry_DRQ { get { Contract.Ensures(Contract.Result<FuncInterp.Entry.DecRefQueue>() != null); return m_FuncEntry_DRQ; } }
+
+        /// <summary>
+        /// FuncInterp DRQ
+        /// </summary>
+        public IDecRefQueue FuncInterp_DRQ { get { Contract.Ensures(Contract.Result<FuncInterp.DecRefQueue>() != null); return m_FuncInterp_DRQ; } }
+
+        /// <summary>
+        /// Goal DRQ
+        /// </summary>
+        public IDecRefQueue Goal_DRQ { get { Contract.Ensures(Contract.Result<Goal.DecRefQueue>() != null); return m_Goal_DRQ; } }
+
+        /// <summary>
+        /// Model DRQ
+        /// </summary>
+        public IDecRefQueue Model_DRQ { get { Contract.Ensures(Contract.Result<Model.DecRefQueue>() != null); return m_Model_DRQ; } }
+
+        /// <summary>
+        /// Params DRQ
+        /// </summary>
+        public IDecRefQueue Params_DRQ { get { Contract.Ensures(Contract.Result<Params.DecRefQueue>() != null); return m_Params_DRQ; } }
+
+        /// <summary>
+        /// ParamDescrs DRQ
+        /// </summary>
+        public IDecRefQueue ParamDescrs_DRQ { get { Contract.Ensures(Contract.Result<ParamDescrs.DecRefQueue>() != null); return m_ParamDescrs_DRQ; } }
+
+        /// <summary>
+        /// Probe DRQ
+        /// </summary>
+        public IDecRefQueue Probe_DRQ { get { Contract.Ensures(Contract.Result<Probe.DecRefQueue>() != null); return m_Probe_DRQ; } }
+
+        /// <summary>
+        /// Solver DRQ
+        /// </summary>
+        public IDecRefQueue Solver_DRQ { get { Contract.Ensures(Contract.Result<Solver.DecRefQueue>() != null); return m_Solver_DRQ; } }
+
+        /// <summary>
+        /// Statistics DRQ
+        /// </summary>
+        public IDecRefQueue Statistics_DRQ { get { Contract.Ensures(Contract.Result<Statistics.DecRefQueue>() != null); return m_Statistics_DRQ; } }
+
+        /// <summary>
+        /// Tactic DRQ
+        /// </summary>
+        public IDecRefQueue Tactic_DRQ { get { Contract.Ensures(Contract.Result<Tactic.DecRefQueue>() != null); return m_Tactic_DRQ; } }
+        
+        /// <summary>
+        /// FixedPoint DRQ
+        /// </summary>
+        public IDecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
 
 
         internal long refCount = 0;
diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs
index 37ae1b110..281ed9ad2 100644
--- a/src/api/dotnet/Fixedpoint.cs
+++ b/src/api/dotnet/Fixedpoint.cs
@@ -337,12 +337,12 @@ namespace Microsoft.Z3
         {
             public DecRefQueue() : base() { }
             public DecRefQueue(uint move_limit) : base(move_limit) { }
-            public override void IncRef(Context ctx, IntPtr obj)
+            internal override void IncRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_fixedpoint_inc_ref(ctx.nCtx, obj);
             }
 
-            public override void DecRef(Context ctx, IntPtr obj)
+            internal override void DecRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_fixedpoint_dec_ref(ctx.nCtx, obj);
             }
diff --git a/src/api/dotnet/FuncInterp.cs b/src/api/dotnet/FuncInterp.cs
index 488abb780..449d460f9 100644
--- a/src/api/dotnet/FuncInterp.cs
+++ b/src/api/dotnet/FuncInterp.cs
@@ -93,12 +93,12 @@ namespace Microsoft.Z3
             {
                 public DecRefQueue() : base() { }
                 public DecRefQueue(uint move_limit) : base(move_limit) { }
-                public override void IncRef(Context ctx, IntPtr obj)
+                internal override void IncRef(Context ctx, IntPtr obj)
                 {
                     Native.Z3_func_entry_inc_ref(ctx.nCtx, obj);
                 }
 
-                public override void DecRef(Context ctx, IntPtr obj)
+                internal override void DecRef(Context ctx, IntPtr obj)
                 {
                     Native.Z3_func_entry_dec_ref(ctx.nCtx, obj);
                 }
@@ -201,12 +201,12 @@ namespace Microsoft.Z3
         {
             public DecRefQueue() : base() { }
             public DecRefQueue(uint move_limit) : base(move_limit) { }
-            public override void IncRef(Context ctx, IntPtr obj)
+            internal override void IncRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_func_interp_inc_ref(ctx.nCtx, obj);
             }
 
-            public override void DecRef(Context ctx, IntPtr obj)
+            internal override void DecRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_func_interp_dec_ref(ctx.nCtx, obj);
             }
diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs
index 13c98f932..46d519d35 100644
--- a/src/api/dotnet/Goal.cs
+++ b/src/api/dotnet/Goal.cs
@@ -221,12 +221,12 @@ namespace Microsoft.Z3
         {
             public DecRefQueue() : base() { }
             public DecRefQueue(uint move_limit) : base(move_limit) { }
-            public override void IncRef(Context ctx, IntPtr obj)
+            internal override void IncRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_goal_inc_ref(ctx.nCtx, obj);
             }
 
-            public override void DecRef(Context ctx, IntPtr obj)
+            internal override void DecRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_goal_dec_ref(ctx.nCtx, obj);
             }
diff --git a/src/api/dotnet/IDecRefQueue.cs b/src/api/dotnet/IDecRefQueue.cs
index a69e28ff2..43506fabf 100644
--- a/src/api/dotnet/IDecRefQueue.cs
+++ b/src/api/dotnet/IDecRefQueue.cs
@@ -25,8 +25,11 @@ using System.Diagnostics.Contracts;
 
 namespace Microsoft.Z3
 {
+    /// <summary>
+    /// DecRefQueue interface
+    /// </summary>
     [ContractClass(typeof(DecRefQueueContracts))]
-    internal abstract class IDecRefQueue
+    public abstract class IDecRefQueue
     {
         #region Object invariant
 
@@ -38,19 +41,25 @@ namespace Microsoft.Z3
 
         #endregion
 
-        readonly internal protected Object m_lock = new Object();
-        readonly internal protected List<IntPtr> m_queue = new List<IntPtr>();
-        internal uint m_move_limit;
+        readonly private Object m_lock = new Object();
+        readonly private List<IntPtr> m_queue = new List<IntPtr>();
+        private uint m_move_limit;
 
-        public IDecRefQueue(uint move_limit = 1024)
+        internal IDecRefQueue(uint move_limit = 1024)
         {
             m_move_limit = move_limit;
         }
 
-        public abstract void IncRef(Context ctx, IntPtr obj);
-        public abstract void DecRef(Context ctx, IntPtr obj);
+        /// <summary>
+        /// Sets the limit on numbers of objects that are kept back at GC collection.
+        /// </summary>
+        /// <param name="l"></param>
+        public void SetLimit(uint l) { m_move_limit = l; }
 
-        public void IncAndClear(Context ctx, IntPtr o)
+        internal abstract void IncRef(Context ctx, IntPtr obj);
+        internal abstract void DecRef(Context ctx, IntPtr obj);
+
+        internal void IncAndClear(Context ctx, IntPtr o)
         {
             Contract.Requires(ctx != null);
 
@@ -58,7 +67,7 @@ namespace Microsoft.Z3
             if (m_queue.Count >= m_move_limit) Clear(ctx);
         }
 
-        public void Add(IntPtr o)
+        internal void Add(IntPtr o)
         {
             if (o == IntPtr.Zero) return;
 
@@ -68,7 +77,7 @@ namespace Microsoft.Z3
             }
         }
 
-        public void Clear(Context ctx)
+        internal void Clear(Context ctx)
         {
             Contract.Requires(ctx != null);
 
@@ -84,12 +93,12 @@ namespace Microsoft.Z3
     [ContractClassFor(typeof(IDecRefQueue))]
     abstract class DecRefQueueContracts : IDecRefQueue
     {
-        public override void IncRef(Context ctx, IntPtr obj)
+        internal override void IncRef(Context ctx, IntPtr obj)
         {
             Contract.Requires(ctx != null);
         }
 
-        public override void DecRef(Context ctx, IntPtr obj)
+        internal override void DecRef(Context ctx, IntPtr obj)
         {
             Contract.Requires(ctx != null);
         }
diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs
index 9cff1e667..adf233a98 100644
--- a/src/api/dotnet/Model.cs
+++ b/src/api/dotnet/Model.cs
@@ -293,12 +293,12 @@ namespace Microsoft.Z3
         {
             public DecRefQueue() : base() { }
             public DecRefQueue(uint move_limit) : base(move_limit) { }
-            public override void IncRef(Context ctx, IntPtr obj)
+            internal override void IncRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_model_inc_ref(ctx.nCtx, obj);
             }
 
-            public override void DecRef(Context ctx, IntPtr obj)
+            internal override void DecRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_model_dec_ref(ctx.nCtx, obj);
             }
diff --git a/src/api/dotnet/ParamDescrs.cs b/src/api/dotnet/ParamDescrs.cs
index a08e11859..af2916faa 100644
--- a/src/api/dotnet/ParamDescrs.cs
+++ b/src/api/dotnet/ParamDescrs.cs
@@ -89,12 +89,12 @@ namespace Microsoft.Z3
         {
             public DecRefQueue() : base() { }
             public DecRefQueue(uint move_limit) : base(move_limit) { }
-            public override void IncRef(Context ctx, IntPtr obj)
+            internal override void IncRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_param_descrs_inc_ref(ctx.nCtx, obj);
             }
 
-            public override void DecRef(Context ctx, IntPtr obj)
+            internal override void DecRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_param_descrs_dec_ref(ctx.nCtx, obj);
             }
diff --git a/src/api/dotnet/Params.cs b/src/api/dotnet/Params.cs
index de2287af5..81ca6727b 100644
--- a/src/api/dotnet/Params.cs
+++ b/src/api/dotnet/Params.cs
@@ -142,12 +142,12 @@ namespace Microsoft.Z3
         {
             public DecRefQueue() : base() { }
             public DecRefQueue(uint move_limit) : base(move_limit) { }
-            public override void IncRef(Context ctx, IntPtr obj)
+            internal override void IncRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_params_inc_ref(ctx.nCtx, obj);
             }
 
-            public override void DecRef(Context ctx, IntPtr obj)
+            internal override void DecRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_params_dec_ref(ctx.nCtx, obj);
             }
diff --git a/src/api/dotnet/Probe.cs b/src/api/dotnet/Probe.cs
index e8907b294..c10755263 100644
--- a/src/api/dotnet/Probe.cs
+++ b/src/api/dotnet/Probe.cs
@@ -75,12 +75,12 @@ namespace Microsoft.Z3
         {
             public DecRefQueue() : base() { }
             public DecRefQueue(uint move_limit) : base(move_limit) { }
-            public override void IncRef(Context ctx, IntPtr obj)
+            internal override void IncRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_probe_inc_ref(ctx.nCtx, obj);
             }
 
-            public override void DecRef(Context ctx, IntPtr obj)
+            internal override void DecRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_probe_dec_ref(ctx.nCtx, obj);
             }
diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs
index 2e12a5842..012a283f5 100644
--- a/src/api/dotnet/Solver.cs
+++ b/src/api/dotnet/Solver.cs
@@ -330,12 +330,12 @@ namespace Microsoft.Z3
         {
             public DecRefQueue() : base() { }
             public DecRefQueue(uint move_limit) : base(move_limit) { }
-            public override void IncRef(Context ctx, IntPtr obj)
+            internal override void IncRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_solver_inc_ref(ctx.nCtx, obj);
             }
 
-            public override void DecRef(Context ctx, IntPtr obj)
+            internal override void DecRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_solver_dec_ref(ctx.nCtx, obj);
             }
diff --git a/src/api/dotnet/Statistics.cs b/src/api/dotnet/Statistics.cs
index 81240e2c0..cf4b703fe 100644
--- a/src/api/dotnet/Statistics.cs
+++ b/src/api/dotnet/Statistics.cs
@@ -191,12 +191,12 @@ namespace Microsoft.Z3
         {
             public DecRefQueue() : base() { }
             public DecRefQueue(uint move_limit) : base(move_limit) { }
-            public override void IncRef(Context ctx, IntPtr obj)
+            internal override void IncRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_stats_inc_ref(ctx.nCtx, obj);
             }
 
-            public override void DecRef(Context ctx, IntPtr obj)
+            internal override void DecRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_stats_dec_ref(ctx.nCtx, obj);
             }
diff --git a/src/api/dotnet/Tactic.cs b/src/api/dotnet/Tactic.cs
index be79c2a43..8399490d5 100644
--- a/src/api/dotnet/Tactic.cs
+++ b/src/api/dotnet/Tactic.cs
@@ -112,16 +112,19 @@ namespace Microsoft.Z3
             Contract.Requires(ctx != null);
         }
 
+        /// <summary>
+        /// DecRefQueue
+        /// </summary>
         internal class DecRefQueue : IDecRefQueue
         {
             public DecRefQueue() : base() { }
             public DecRefQueue(uint move_limit) : base(move_limit) { }
-            public override void IncRef(Context ctx, IntPtr obj)
+            internal override void IncRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_tactic_inc_ref(ctx.nCtx, obj);
             }
 
-            public override void DecRef(Context ctx, IntPtr obj)
+            internal override void DecRef(Context ctx, IntPtr obj)
             {
                 Native.Z3_tactic_dec_ref(ctx.nCtx, obj);
             }
diff --git a/src/api/java/AST.java b/src/api/java/AST.java
index fdb1643a5..870f1d5d3 100644
--- a/src/api/java/AST.java
+++ b/src/api/java/AST.java
@@ -229,7 +229,7 @@ public class AST extends Z3Object
         // Console.WriteLine("AST IncRef()");
         if (getContext() == null || o == 0)
             return;
-        getContext().ast_DRQ().incAndClear(getContext(), o);
+        getContext().getASTDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
@@ -238,7 +238,7 @@ public class AST extends Z3Object
         // Console.WriteLine("AST DecRef()");
         if (getContext() == null || o == 0)
             return;
-        getContext().ast_DRQ().add(o);
+        getContext().getASTDRQ().add(o);
         super.decRef(o);
     }
 
diff --git a/src/api/java/ASTMap.java b/src/api/java/ASTMap.java
index 96ddfbf76..a37e9d0ff 100644
--- a/src/api/java/ASTMap.java
+++ b/src/api/java/ASTMap.java
@@ -124,13 +124,13 @@ class ASTMap extends Z3Object
 
     void incRef(long o) throws Z3Exception
     {
-        getContext().astmap_DRQ().incAndClear(getContext(), o);
+        getContext().getASTMapDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
     void decRef(long o) throws Z3Exception
     {
-        getContext().astmap_DRQ().add(o);
+        getContext().getASTMapDRQ().add(o);
         super.decRef(o);
     }
 }
diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java
index 30c96e2e7..48c079ecc 100644
--- a/src/api/java/ASTVector.java
+++ b/src/api/java/ASTVector.java
@@ -110,13 +110,13 @@ class ASTVector extends Z3Object
 
     void incRef(long o) throws Z3Exception
     {
-        getContext().astvector_DRQ().incAndClear(getContext(), o);
+        getContext().getASTVectorDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
     void decRef(long o) throws Z3Exception
     {
-        getContext().astvector_DRQ().add(o);
+        getContext().getASTVectorDRQ().add(o);
         super.decRef(o);
     }
 }
diff --git a/src/api/java/ApplyResult.java b/src/api/java/ApplyResult.java
index d21a78a9c..8e998111f 100644
--- a/src/api/java/ApplyResult.java
+++ b/src/api/java/ApplyResult.java
@@ -81,13 +81,13 @@ public class ApplyResult extends Z3Object
 
     void incRef(long o) throws Z3Exception
     {
-        getContext().applyResult_DRQ().incAndClear(getContext(), o);
+        getContext().getApplyResultDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
     void decRef(long o) throws Z3Exception
     {
-        getContext().applyResult_DRQ().add(o);
+        getContext().getApplyResultDRQ().add(o);
         super.decRef(o);
     }
 }
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 42fd0f7e1..e9dd42dc0 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -3674,77 +3674,77 @@ public class Context extends IDisposable
     private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue(10);
     private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue(10);
 
-    ASTDecRefQueue ast_DRQ()
+    public IDecRefQueue getASTDRQ()
     {
         return m_AST_DRQ;
     }
 
-    ASTMapDecRefQueue astmap_DRQ()
+    public IDecRefQueue getASTMapDRQ()
     {
         return m_ASTMap_DRQ;
     }
 
-    ASTVectorDecRefQueue astvector_DRQ()
+    public IDecRefQueue getASTVectorDRQ()
     {
         return m_ASTVector_DRQ;
     }
 
-    ApplyResultDecRefQueue applyResult_DRQ()
+    public IDecRefQueue getApplyResultDRQ()
     {
         return m_ApplyResult_DRQ;
     }
 
-    FuncInterpEntryDecRefQueue funcEntry_DRQ()
+    public IDecRefQueue getFuncEntryDRQ()
     {
         return m_FuncEntry_DRQ;
     }
 
-    FuncInterpDecRefQueue funcInterp_DRQ()
+    public IDecRefQueue getFuncInterpDRQ()
     {
         return m_FuncInterp_DRQ;
     }
 
-    GoalDecRefQueue goal_DRQ()
+    public IDecRefQueue getGoalDRQ()
     {
         return m_Goal_DRQ;
     }
 
-    ModelDecRefQueue model_DRQ()
+    public IDecRefQueue getModelDRQ()
     {
         return m_Model_DRQ;
     }
 
-    ParamsDecRefQueue params_DRQ()
+    public IDecRefQueue getParamsDRQ()
     {
         return m_Params_DRQ;
     }
 
-    ParamDescrsDecRefQueue paramDescrs_DRQ()
+    public IDecRefQueue getParamDescrsDRQ()
     {
         return m_ParamDescrs_DRQ;
     }
 
-    ProbeDecRefQueue probe_DRQ()
+    public IDecRefQueue getProbeDRQ()
     {
         return m_Probe_DRQ;
     }
 
-    SolverDecRefQueue solver_DRQ()
+    public IDecRefQueue getSolverDRQ()
     {
         return m_Solver_DRQ;
     }
 
-    StatisticsDecRefQueue statistics_DRQ()
+    public IDecRefQueue getStatisticsDRQ()
     {
         return m_Statistics_DRQ;
     }
 
-    TacticDecRefQueue tactic_DRQ()
+    public IDecRefQueue getTacticDRQ()
     {
         return m_Tactic_DRQ;
     }
 
-    FixedpointDecRefQueue fixedpoint_DRQ()
+    public IDecRefQueue getFixedpointDRQ()
     {
         return m_Fixedpoint_DRQ;
     }
diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java
index 808785ddc..624a527fd 100644
--- a/src/api/java/Fixedpoint.java
+++ b/src/api/java/Fixedpoint.java
@@ -334,13 +334,13 @@ public class Fixedpoint extends Z3Object
 
     void incRef(long o) throws Z3Exception
     {
-        getContext().fixedpoint_DRQ().incAndClear(getContext(), o);
+        getContext().getFixedpointDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
     void decRef(long o) throws Z3Exception
     {
-        getContext().fixedpoint_DRQ().add(o);
+        getContext().getFixedpointDRQ().add(o);
         super.decRef(o);
     }
 }
diff --git a/src/api/java/FuncInterp.java b/src/api/java/FuncInterp.java
index 7fb5ac13e..31f37a4ba 100644
--- a/src/api/java/FuncInterp.java
+++ b/src/api/java/FuncInterp.java
@@ -93,13 +93,13 @@ public class FuncInterp extends Z3Object
 
         void incRef(long o) throws Z3Exception
         {
-            getContext().funcEntry_DRQ().incAndClear(getContext(), o);
+            getContext().getFuncEntryDRQ().incAndClear(getContext(), o);
             super.incRef(o);
         }
 
         void decRef(long o) throws Z3Exception
         {
-            getContext().funcEntry_DRQ().add(o);
+            getContext().getFuncEntryDRQ().add(o);
             super.decRef(o);
         }
     };
@@ -194,13 +194,13 @@ public class FuncInterp extends Z3Object
 
     void incRef(long o) throws Z3Exception
     {
-        getContext().funcInterp_DRQ().incAndClear(getContext(), o);
+        getContext().getFuncInterpDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
     void decRef(long o) throws Z3Exception
     {
-        getContext().funcInterp_DRQ().add(o);
+        getContext().getFuncInterpDRQ().add(o);
         super.decRef(o);
     }
 }
diff --git a/src/api/java/Goal.java b/src/api/java/Goal.java
index b6897c517..64f2e0acb 100644
--- a/src/api/java/Goal.java
+++ b/src/api/java/Goal.java
@@ -236,13 +236,13 @@ public class Goal extends Z3Object
 
     void incRef(long o) throws Z3Exception
     {
-        getContext().goal_DRQ().incAndClear(getContext(), o);
+        getContext().getGoalDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
     void decRef(long o) throws Z3Exception
     {
-        getContext().goal_DRQ().add(o);
+        getContext().getGoalDRQ().add(o);
         super.decRef(o);
     }
 
diff --git a/src/api/java/IDecRefQueue.java b/src/api/java/IDecRefQueue.java
index e8cab3477..823288a20 100644
--- a/src/api/java/IDecRefQueue.java
+++ b/src/api/java/IDecRefQueue.java
@@ -19,22 +19,24 @@ package com.microsoft.z3;
 
 import java.util.LinkedList;
 
-abstract class IDecRefQueue
+public abstract class IDecRefQueue
 {
     protected Object m_lock = new Object();
     protected LinkedList<Long> m_queue = new LinkedList<Long>();
     protected int m_move_limit;
 
-    public IDecRefQueue() 
-    {
-    m_move_limit = 1024;
+    protected IDecRefQueue() 
+	{
+    	m_move_limit = 1024;
     }
 
-    public IDecRefQueue(int move_limit) 
+    protected IDecRefQueue(int move_limit) 
     {
-    m_move_limit = move_limit;
+    	m_move_limit = move_limit;
     }
-
+ 
+    public void setLimit(int l) { m_move_limit = l; }
+ 
     protected abstract void incRef(Context ctx, long obj);
 
     protected abstract void decRef(Context ctx, long obj);
diff --git a/src/api/java/Model.java b/src/api/java/Model.java
index 9392aacb6..3d68d5485 100644
--- a/src/api/java/Model.java
+++ b/src/api/java/Model.java
@@ -303,13 +303,13 @@ public class Model extends Z3Object
 
     void incRef(long o) throws Z3Exception
     {
-        getContext().model_DRQ().incAndClear(getContext(), o);
+        getContext().getModelDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
     void decRef(long o) throws Z3Exception
     {
-        getContext().model_DRQ().add(o);
+        getContext().getModelDRQ().add(o);
         super.decRef(o);
     }
 }
diff --git a/src/api/java/ParamDescrs.java b/src/api/java/ParamDescrs.java
index 4afae9f76..e1f0d16e5 100644
--- a/src/api/java/ParamDescrs.java
+++ b/src/api/java/ParamDescrs.java
@@ -90,13 +90,13 @@ public class ParamDescrs extends Z3Object
 
     void incRef(long o) throws Z3Exception
     {
-        getContext().paramDescrs_DRQ().incAndClear(getContext(), o);
+        getContext().getParamDescrsDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
     void decRef(long o) throws Z3Exception
     {
-        getContext().paramDescrs_DRQ().add(o);
+        getContext().getParamDescrsDRQ().add(o);
         super.decRef(o);
     }
 }
diff --git a/src/api/java/Params.java b/src/api/java/Params.java
index bbe6d66cf..693491f41 100644
--- a/src/api/java/Params.java
+++ b/src/api/java/Params.java
@@ -130,13 +130,13 @@ public class Params extends Z3Object
 
     void incRef(long o) throws Z3Exception
     {
-        getContext().params_DRQ().incAndClear(getContext(), o);
+        getContext().getParamsDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
     void decRef(long o) throws Z3Exception
     {
-        getContext().params_DRQ().add(o);
+        getContext().getParamsDRQ().add(o);
         super.decRef(o);
     }
 }
diff --git a/src/api/java/Probe.java b/src/api/java/Probe.java
index 335bd038c..62b0612b9 100644
--- a/src/api/java/Probe.java
+++ b/src/api/java/Probe.java
@@ -53,13 +53,13 @@ public class Probe extends Z3Object
 
     void incRef(long o) throws Z3Exception
     {
-        getContext().probe_DRQ().incAndClear(getContext(), o);
+        getContext().getProbeDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
     void decRef(long o) throws Z3Exception
     {
-        getContext().probe_DRQ().add(o);
+        getContext().getProbeDRQ().add(o);
         super.decRef(o);
     }
 }
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index 3e66a29ac..4b330ff86 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -337,13 +337,13 @@ public class Solver extends Z3Object
 
     void incRef(long o) throws Z3Exception
     {
-        getContext().solver_DRQ().incAndClear(getContext(), o);
+        getContext().getSolverDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
     void decRef(long o) throws Z3Exception
     {
-        getContext().solver_DRQ().add(o);
+        getContext().getSolverDRQ().add(o);
         super.decRef(o);
     }
 }
diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java
index 475352024..aa909b9bd 100644
--- a/src/api/java/Statistics.java
+++ b/src/api/java/Statistics.java
@@ -199,13 +199,13 @@ public class Statistics extends Z3Object
 
     void incRef(long o) throws Z3Exception
     {
-        getContext().statistics_DRQ().incAndClear(getContext(), o);
+        getContext().getStatisticsDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
     void decRef(long o) throws Z3Exception
     {
-        getContext().statistics_DRQ().add(o);
+        getContext().getStatisticsDRQ().add(o);
         super.decRef(o);
     }
 }
diff --git a/src/api/java/Tactic.java b/src/api/java/Tactic.java
index 79f60e497..65404a927 100644
--- a/src/api/java/Tactic.java
+++ b/src/api/java/Tactic.java
@@ -94,13 +94,13 @@ public class Tactic extends Z3Object
 
     void incRef(long o) throws Z3Exception
     {
-        getContext().tactic_DRQ().incAndClear(getContext(), o);
+        getContext().getTacticDRQ().incAndClear(getContext(), o);
         super.incRef(o);
     }
 
     void decRef(long o) throws Z3Exception
     {
-        getContext().tactic_DRQ().add(o);
+        getContext().getTacticDRQ().add(o);
         super.decRef(o);
     }
 }