mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
Remove redundant cast
This commit is contained in:
parent
93ad8d32b9
commit
54e5bf2422
|
@ -46,7 +46,7 @@ public class ConstructorList extends Z3Object
|
||||||
super(ctx);
|
super(ctx);
|
||||||
|
|
||||||
setNativeObject(Native.mkConstructorList(getContext().nCtx(),
|
setNativeObject(Native.mkConstructorList(getContext().nCtx(),
|
||||||
(int) constructors.length,
|
constructors.length,
|
||||||
Constructor.arrayToNative(constructors)));
|
Constructor.arrayToNative(constructors)));
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -373,7 +373,7 @@ public class Context extends IDisposable
|
||||||
|
|
||||||
{
|
{
|
||||||
checkContextMatch(names);
|
checkContextMatch(names);
|
||||||
int n = (int) names.length;
|
int n = names.length;
|
||||||
ConstructorList[] cla = new ConstructorList[n];
|
ConstructorList[] cla = new ConstructorList[n];
|
||||||
long[] n_constr = new long[n];
|
long[] n_constr = new long[n];
|
||||||
for (int i = 0; i < n; i++)
|
for (int i = 0; i < n; i++)
|
||||||
|
@ -2384,7 +2384,7 @@ public class Context extends IDisposable
|
||||||
{
|
{
|
||||||
|
|
||||||
return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
|
return Native.benchmarkToSmtlibString(nCtx(), name, logic, status,
|
||||||
attributes, (int) assumptions.length,
|
attributes, assumptions.length,
|
||||||
AST.arrayToNative(assumptions), formula.getNativeObject());
|
AST.arrayToNative(assumptions), formula.getNativeObject());
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -101,7 +101,7 @@ public class DatatypeSort extends Sort
|
||||||
|
|
||||||
{
|
{
|
||||||
super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),
|
super(ctx, Native.mkDatatype(ctx.nCtx(), name.getNativeObject(),
|
||||||
(int) constructors.length, arrayToNative(constructors)));
|
constructors.length, arrayToNative(constructors)));
|
||||||
|
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
|
@ -98,7 +98,7 @@ public class EnumSort extends Sort
|
||||||
long[] n_constdecls = new long[n];
|
long[] n_constdecls = new long[n];
|
||||||
long[] n_testers = new long[n];
|
long[] n_testers = new long[n];
|
||||||
setNativeObject(Native.mkEnumerationSort(ctx.nCtx(),
|
setNativeObject(Native.mkEnumerationSort(ctx.nCtx(),
|
||||||
name.getNativeObject(), (int) n, Symbol.arrayToNative(enumNames),
|
name.getNativeObject(), n, Symbol.arrayToNative(enumNames),
|
||||||
n_constdecls, n_testers));
|
n_constdecls, n_testers));
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
Loading…
Reference in a new issue