From c045214da2f25857134dcb203b343beb4c54d703 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 27 Nov 2012 16:37:04 +0000 Subject: [PATCH] Managed API: Bugfixes and refactoring. Signed-off-by: Christoph M. Wintersteiger --- src/api/dotnet/Expr.cs | 2 ++ src/api/dotnet/Quantifier.cs | 2 -- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index 6c2ebb3ad..dade77eb1 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -1533,6 +1533,7 @@ namespace Microsoft.Z3 case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj); case Z3_sort_kind.Z3_REAL_SORT: return new RatNum(ctx, obj); case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj); + case Z3_sort_kind.Z3_UNKNOWN_SORT: throw new Z3Exception("Unknown Sort"); } } @@ -1544,6 +1545,7 @@ namespace Microsoft.Z3 case Z3_sort_kind.Z3_BV_SORT: return new BitVecExpr(ctx, obj); case Z3_sort_kind.Z3_ARRAY_SORT: return new ArrayExpr(ctx, obj); case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj); + case Z3_sort_kind.Z3_UNKNOWN_SORT: throw new Z3Exception("Unknown Sort"); } return new Expr(ctx, obj); diff --git a/src/api/dotnet/Quantifier.cs b/src/api/dotnet/Quantifier.cs index c6754e570..f59d0bda2 100644 --- a/src/api/dotnet/Quantifier.cs +++ b/src/api/dotnet/Quantifier.cs @@ -181,8 +181,6 @@ namespace Microsoft.Z3 if (sorts.Length != names.Length) throw new Z3Exception("Number of sorts does not match number of names"); - IntPtr[] _patterns = AST.ArrayToNative(patterns); - if (noPatterns == null && quantifierID == null && skolemID == null) { NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) ? 1 : 0, weight,