mirror of
https://github.com/Z3Prover/z3
synced 2026-06-04 16:10:50 +00:00
check context match
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
018461e60d
commit
b769ca3639
1 changed files with 2 additions and 1 deletions
|
|
@ -2865,7 +2865,8 @@ namespace Microsoft.Z3
|
||||||
Debug.Assert(i != null);
|
Debug.Assert(i != null);
|
||||||
Debug.Assert(a != null);
|
Debug.Assert(a != null);
|
||||||
Debug.Assert(s != null);
|
Debug.Assert(s != null);
|
||||||
CheckContextMatch(f, i, a, s);
|
CheckContextMatch(f, i, a);
|
||||||
|
CheckContextMatch(s, a);
|
||||||
return Expr.Create(this, Native.Z3_mk_seq_foldli(nCtx, f.NativeObject, i.NativeObject, a.NativeObject, s.NativeObject));
|
return Expr.Create(this, Native.Z3_mk_seq_foldli(nCtx, f.NativeObject, i.NativeObject, a.NativeObject, s.NativeObject));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue