diff --git a/src/api/java/ConstructorList.java b/src/api/java/ConstructorList.java index a50ff11ea..fe3fae1ac 100644 --- a/src/api/java/ConstructorList.java +++ b/src/api/java/ConstructorList.java @@ -46,7 +46,7 @@ public class ConstructorList extends Z3Object super(ctx); setNativeObject(Native.mkConstructorList(getContext().nCtx(), - (int) constructors.length, + constructors.length, Constructor.arrayToNative(constructors))); } } diff --git a/src/api/java/Context.java b/src/api/java/Context.java index f1baa92f2..eb51af101 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -373,7 +373,7 @@ public class Context extends IDisposable { checkContextMatch(names); - int n = (int) names.length; + int n = names.length; ConstructorList[] cla = new ConstructorList[n]; long[] n_constr = new long[n]; for (int i = 0; i < n; i++) @@ -2384,7 +2384,7 @@ public class Context extends IDisposable { return Native.benchmarkToSmtlibString(nCtx(), name, logic, status, - attributes, (int) assumptions.length, + attributes, assumptions.length, AST.arrayToNative(assumptions), formula.getNativeObject()); } diff --git a/src/api/java/DatatypeSort.java b/src/api/java/DatatypeSort.java index d7896b15f..644d434d3 100644 --- a/src/api/java/DatatypeSort.java +++ b/src/api/java/DatatypeSort.java @@ -101,7 +101,7 @@ public class DatatypeSort extends Sort { super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(), - (int) constructors.length, arrayToNative(constructors))); + constructors.length, arrayToNative(constructors))); } }; diff --git a/src/api/java/EnumSort.java b/src/api/java/EnumSort.java index da471f5ea..bb60eef56 100644 --- a/src/api/java/EnumSort.java +++ b/src/api/java/EnumSort.java @@ -98,7 +98,7 @@ public class EnumSort extends Sort long[] n_constdecls = new long[n]; long[] n_testers = new long[n]; setNativeObject(Native.mkEnumerationSort(ctx.nCtx(), - name.getNativeObject(), (int) n, Symbol.arrayToNative(enumNames), + name.getNativeObject(), n, Symbol.arrayToNative(enumNames), n_constdecls, n_testers)); } };