From 8c32f6b01558b1ce34c89d6e29be030f84c66f63 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 27 Nov 2012 00:38:19 +0000 Subject: [PATCH] Managed API: Refactoring Signed-off-by: Christoph M. Wintersteiger --- src/api/dotnet/FuncDecl.cs | 2 +- src/api/dotnet/Goal.cs | 6 +++--- src/api/dotnet/Model.cs | 4 ++-- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs index 37929e88f..15b6a59db 100644 --- a/src/api/dotnet/FuncDecl.cs +++ b/src/api/dotnet/FuncDecl.cs @@ -110,7 +110,7 @@ namespace Microsoft.Z3 { Contract.Ensures(Contract.Result() != null); - var n = DomainSize; + uint n = DomainSize; Sort[] res = new Sort[n]; for (uint i = 0; i < n; i++) diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs index 6a0b253bb..e648ac80c 100644 --- a/src/api/dotnet/Goal.cs +++ b/src/api/dotnet/Goal.cs @@ -184,10 +184,10 @@ namespace Microsoft.Z3 { Tactic t = Context.MkTactic("simplify"); ApplyResult res = t.Apply(this, p); - + if (res.NumSubgoals == 0) - return Context.MkGoal(); - else + throw new Z3Exception("No subgoals"); + else return res.Subgoals[0]; } diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs index 5529677dd..5c0bc24f8 100644 --- a/src/api/dotnet/Model.cs +++ b/src/api/dotnet/Model.cs @@ -165,8 +165,8 @@ namespace Microsoft.Z3 { Contract.Ensures(Contract.Result() != null); - var nFuncs = NumFuncs; - var nConsts = NumConsts; + uint nFuncs = NumFuncs; + uint nConsts = NumConsts; uint n = nFuncs + nConsts; FuncDecl[] res = new FuncDecl[n]; for (uint i = 0; i < nConsts; i++)