mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 12:28:44 +00:00
replace long by int
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
87c3b5ee51
commit
ab6abe901f
|
@ -2026,7 +2026,7 @@ public class Context implements AutoCloseable {
|
|||
/**
|
||||
* Take the lower and upper-bounded Kleene star of a regular expression.
|
||||
*/
|
||||
public ReExpr mkLoop(ReExpr re, long lo, long hi)
|
||||
public ReExpr mkLoop(ReExpr re, int lo, int hi)
|
||||
{
|
||||
return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, hi));
|
||||
}
|
||||
|
@ -2034,7 +2034,7 @@ public class Context implements AutoCloseable {
|
|||
/**
|
||||
* Take the lower-bounded Kleene star of a regular expression.
|
||||
*/
|
||||
public ReExpr mkLoop(ReExpr re, long lo)
|
||||
public ReExpr mkLoop(ReExpr re, int lo)
|
||||
{
|
||||
return (ReExpr) Expr.create(this, Native.mkReLoop(nCtx(), re.getNativeObject(), lo, 0));
|
||||
}
|
||||
|
@ -2090,7 +2090,7 @@ public class Context implements AutoCloseable {
|
|||
/**
|
||||
* Create an at-most-k constraint.
|
||||
*/
|
||||
public BoolExpr mkAtMost(BoolExpr[] args, loong k)
|
||||
public BoolExpr mkAtMost(BoolExpr[] args, long k)
|
||||
{
|
||||
checkContextMatch(args);
|
||||
return (BoolExpr) Expr.create(this, Native.mkAtmost(nCtx(), args.length, AST.arrayToNative(args), k));
|
||||
|
|
Loading…
Reference in a new issue