mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
correct the type returned by mkNth #4454
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
7ac2791482
commit
0bc33e9c9d
|
@ -2488,12 +2488,12 @@ namespace Microsoft.Z3
|
|||
/// <summary>
|
||||
/// Retrieve element at index.
|
||||
/// </summary>
|
||||
public SeqExpr MkNth(SeqExpr s, Expr index)
|
||||
public Expr MkNth(SeqExpr s, Expr index)
|
||||
{
|
||||
Debug.Assert(s != null);
|
||||
Debug.Assert(index != null);
|
||||
CheckContextMatch(s, index);
|
||||
return new SeqExpr(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject));
|
||||
return Expr.Create(this, Native.Z3_mk_seq_nth(nCtx, s.NativeObject, index.NativeObject));
|
||||
}
|
||||
|
||||
/// <summary>
|
||||
|
|
|
@ -2051,10 +2051,10 @@ public class Context implements AutoCloseable {
|
|||
/**
|
||||
* Retrieve element at index.
|
||||
*/
|
||||
public SeqExpr MkNth(SeqExpr s, Expr index)
|
||||
public Expr MkNth(SeqExpr s, Expr index)
|
||||
{
|
||||
checkContextMatch(s, index);
|
||||
return (SeqExpr) Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject()));
|
||||
return Expr.create(this, Native.mkSeqNth(nCtx(), s.getNativeObject(), index.getNativeObject()));
|
||||
}
|
||||
|
||||
|
||||
|
|
Loading…
Reference in a new issue