mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-05 18:05:15 +00:00
Code Activity

Add 4-parameter checkContextMatch overload for consistency

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-01-17 19:01:33 +00:00
parent 624c3a3663
commit e483213248
1 changed files with 9 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2271,7 +2271,7 @@ public class Context implements AutoCloseable {
*/ */
public final <R extends Sort, A extends Sort> Expr<A> mkSeqFoldli(Expr<?> f, Expr<IntSort> i, Expr<A> a, Expr<SeqSort<R>> s) public final <R extends Sort, A extends Sort> Expr<A> mkSeqFoldli(Expr<?> f, Expr<IntSort> i, Expr<A> a, Expr<SeqSort<R>> s)
{ {
checkContextMatch(new Z3Object[] { f, i, a, s }); checkContextMatch(f, i, a, s);
return (Expr<A>) Expr.create(this, Native.mkSeqFoldli(nCtx(), f.getNativeObject(), i.getNativeObject(), a.getNativeObject(), s.getNativeObject())); return (Expr<A>) Expr.create(this, Native.mkSeqFoldli(nCtx(), f.getNativeObject(), i.getNativeObject(), a.getNativeObject(), s.getNativeObject()));
} }
@ -4470,6 +4470,14 @@ public class Context implements AutoCloseable {
checkContextMatch(other3); checkContextMatch(other3);
} }
void checkContextMatch(Z3Object other1, Z3Object other2, Z3Object other3, Z3Object other4)
{
checkContextMatch(other1);
checkContextMatch(other2);
checkContextMatch(other3);
checkContextMatch(other4);
}
void checkContextMatch(Z3Object[] arr) void checkContextMatch(Z3Object[] arr)
{ {
if (arr != null) if (arr != null)