diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 3519900cd..b903f71e0 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -3083,8 +3083,6 @@ public class Context extends IDisposable **/ protected void finalize() { - // Console.WriteLine("Context Finalizer from " + - // System.Threading.Thread.CurrentThread.ManagedThreadId); Dispose(); if (m_refCount == 0) @@ -3094,6 +3092,7 @@ public class Context extends IDisposable m_ctx = 0; } else /* re-queue the finalizer */ + /* BUG: DRQ's need to be taken over too! */ new Context(m_ctx, m_refCount, m_n_err_handler); } @@ -3102,8 +3101,6 @@ public class Context extends IDisposable **/ public void Dispose() { - // Console.WriteLine("Context Dispose from " + - // System.Threading.Thread.CurrentThread.ManagedThreadId); m_AST_DRQ.Clear(this); m_ASTMap_DRQ.Clear(this); m_ASTVector_DRQ.Clear(this); diff --git a/src/api/java/Z3Object.java b/src/api/java/Z3Object.java index e5e4af3c2..877fead79 100644 --- a/src/api/java/Z3Object.java +++ b/src/api/java/Z3Object.java @@ -104,13 +104,12 @@ public class Z3Object extends IDisposable return null; long[] an = new long[a.length]; for (int i = 0; i < a.length; i++) - if (a[i] != null) - an[i] = a[i].NativeObject(); + an[i] = a[i].NativeObject(); return an; } static int ArrayLength(Z3Object[] a) { - return (a == null) ? 0 : (int) a.length; + return (a == null) ? 0 : a.length; } }