mirror of
https://github.com/Z3Prover/z3
synced 2025-06-13 09:26:15 +00:00
This commit is contained in:
parent
6670807103
commit
b386b84f34
1 changed files with 1 additions and 1 deletions
|
@ -2185,7 +2185,7 @@ public class Context implements AutoCloseable {
|
||||||
/**
|
/**
|
||||||
* Check for regular expression membership.
|
* Check for regular expression membership.
|
||||||
*/
|
*/
|
||||||
public final <R extends Sort> BoolExpr mkInRe(Expr<SeqSort<R>> s, Expr<ReSort<R>> re)
|
public final <R extends Sort> BoolExpr mkInRe(Expr<SeqSort<R>> s, ReExpr<SeqSort<R>> re)
|
||||||
{
|
{
|
||||||
checkContextMatch(s, re);
|
checkContextMatch(s, re);
|
||||||
return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
|
return (BoolExpr) Expr.create(this, Native.mkSeqInRe(nCtx(), s.getNativeObject(), re.getNativeObject()));
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue