diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 629e96484..4892ab4ec 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -880,10 +880,7 @@ namespace Microsoft.Z3 { Debug.Assert(f != null); Debug.Assert(args == null || args.All(a => a != null)); - - CheckContextMatch(f); - CheckContextMatch(args); - return Expr.Create(this, f, args.ToArray()); + return MkApp(f, args?.ToArray()); } #region Propositional @@ -1051,10 +1048,7 @@ namespace Microsoft.Z3 public BoolExpr MkAnd(IEnumerable t) { Debug.Assert(t != null); - Debug.Assert(t.All(a => a != null)); - CheckContextMatch(t); - var ands = t.ToArray(); - return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.ArrayToNative(ands))); + return MkAnd(t.ToArray()); } /// @@ -1076,11 +1070,7 @@ namespace Microsoft.Z3 public BoolExpr MkOr(IEnumerable t) { Debug.Assert(t != null); - Debug.Assert(t.All(a => a != null)); - - CheckContextMatch(t); - var ts = t.ToArray(); - return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)ts.Length, AST.ArrayToNative(ts))); + return MkOr(t.ToArray()); } #endregion @@ -1104,11 +1094,7 @@ namespace Microsoft.Z3 public ArithExpr MkAdd(IEnumerable t) { Debug.Assert(t != null); - Debug.Assert(t.All(a => a != null)); - - CheckContextMatch(t); - var ts = t.ToArray(); - return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)ts.Length, AST.ArrayToNative(ts))); + return MkAdd(t.ToArray()); } /// @@ -1120,8 +1106,7 @@ namespace Microsoft.Z3 Debug.Assert(t.All(a => a != null)); CheckContextMatch(t); - var ts = t.ToArray(); - return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)ts.Length, AST.ArrayToNative(ts))); + return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } /// @@ -1130,11 +1115,7 @@ namespace Microsoft.Z3 public ArithExpr MkMul(IEnumerable t) { Debug.Assert(t != null); - Debug.Assert(t.All(a => a != null)); - - CheckContextMatch(t); - var ts = t.ToArray(); - return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)ts.Length, AST.ArrayToNative(ts))); + return MkMul(t.ToArray()); } ///