diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index cf235b4af..b37dc12d7 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -1055,6 +1055,19 @@ namespace Microsoft.Z3 return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } + /// <summary> + /// Create an expression representing <c>t[0] * t[1] * ...</c>. + /// </summary> + public ArithExpr MkMul(IEnumerable<ArithExpr> t) + { + Contract.Requires(t != null); + Contract.Requires(Contract.ForAll(t, a => a != null)); + Contract.Ensures(Contract.Result<ArithExpr>() != null); + + CheckContextMatch(t); + return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Count(), AST.EnumToNative(t))); + } + /// <summary> /// Create an expression representing <c>t[0] - t[1] - ...</c>. /// </summary>