diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 3ad136f12..5277dab38 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -39,13 +39,6 @@ public class Context extends IDisposable initContext(); } - private Context(long ctx, long refCount) - { - super(); - this.m_ctx = ctx; - this.m_refCount = refCount; - } - /** * Creates a new symbol using an integer. Not all integers can be * passed to this function. The legal range of unsigned integers is 0 to diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index 58f7638ba..381b9b0ae 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -128,7 +128,8 @@ public class Sort extends AST static Sort create(Context ctx, long obj) throws Z3Exception { - switch (Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), obj))) + Z3_sort_kind sk = Z3_sort_kind.fromInt(Native.getSortKind(ctx.nCtx(), obj)); + switch (sk) { case Z3_ARRAY_SORT: return new ArraySort(ctx, obj);