mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Update the mkConstant parameter type (#4996)

Browse source
This commit is contained in:
Malte Mues 2021-02-05 01:17:49 +01:00 committed by GitHub
parent 0ec567fe15
commit 5d8d42b1fa
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/java/Context.java
View file

@ -2018,7 +2018,7 @@ public class Context implements AutoCloseable {
/** /**
* Concatenate sequences. * Concatenate sequences.
*/ */
public <R extends Sort> SeqExpr<R> mkConcat(SeqSort<R>... t) public <R extends Sort> SeqExpr<R> mkConcat(Expr<SeqSort<R>>... t)
{ {
checkContextMatch(t); checkContextMatch(t);
return (SeqExpr<R>) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t))); return (SeqExpr<R>) Expr.create(this, Native.mkSeqConcat(nCtx(), t.length, AST.arrayToNative(t)));