mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

fixes to dotnet interface

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-26 17:14:29 -08:00
parent a0e98ca39b
commit 58f8181a74
4 changed files with 16 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/api/api_opt.cpp
View file

@ -129,12 +129,13 @@ extern "C" {
RESET_ERROR_CODE();
model_ref _m;
to_optimize_ref(o).get_model(_m);
if (!_m) {
SET_ERROR_CODE(Z3_INVALID_USAGE);
RETURN_Z3(0);
}
Z3_model_ref * m_ref = alloc(Z3_model_ref);
m_ref->m_model = _m;
if (_m) {
m_ref->m_model = _m;
}
else {
m_ref->m_model = alloc(model, mk_c(c)->m());
}
mk_c(c)->save_object(m_ref);
RETURN_Z3(of_model(m_ref));
Z3_CATCH_RETURN(0);

4
src/api/dotnet/Optimize.cs
View file

@ -142,12 +142,12 @@ namespace Microsoft.Z3
public ArithExpr GetLower(uint index)
{
return new ArithExpr(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
}
public ArithExpr GetUpper(uint index)
{
return new ArithExpr(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
}
public override string ToString()