diff --git a/src/api/dotnet/ArrayExpr.cs b/src/api/dotnet/ArrayExpr.cs index d0e45561d..5fc27d253 100644 --- a/src/api/dotnet/ArrayExpr.cs +++ b/src/api/dotnet/ArrayExpr.cs @@ -44,5 +44,10 @@ namespace Microsoft.Z3 get { return Context.MkSelect(this, index); } } + public Expr this[IEnumerable index] + { + get { return Context.MkSelect(this, index.ToArray()); } + } + } } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 150283ea5..c5222d340 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2079,6 +2079,7 @@ namespace Microsoft.Z3 return Expr.Create(this, Native.Z3_mk_select_n(nCtx, a.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args))); } + /// /// Array update. ///