diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index c3c33a41e..421c81fae 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -2609,6 +2609,19 @@ namespace Microsoft.Z3 CheckContextMatch(t); return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t))); } + + + /// + /// Create a range expression. + /// + public ReExpr MkRange(SeqExpr lo, SeqExpr hi) + { + Contract.Requires(lo != null); + Contract.Requires(hi != null); + Contract.Ensures(Contract.Result() != null); + CheckContextMatch(lo, hi); + return new ReExpr(this, Native.Z3_mk_re_range(nCtx, lo.NativeObject, hi.NativeObject)); + } #endregion