From 0cf1f9c2106ee7110465809f0fd000946c9d0e9a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 14 Aug 2014 12:15:58 +0100 Subject: [PATCH 1/2] .NET API context refcounting; changed int to long to be on the safe side on 64-bit platforms. Signed-off-by: Christoph M. Wintersteiger --- src/api/dotnet/Context.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 5436fe0a0..2b88cbab7 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -3646,7 +3646,7 @@ namespace Microsoft.Z3 internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_Fixedpoint_DRQ; } } - internal int refCount = 0; + internal long refCount = 0; /// /// Finalizer. From 37ed4b04d078d6d1e35db2799d769e8d4b87f775 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 14 Aug 2014 12:18:00 +0100 Subject: [PATCH 2/2] Bugfix: param_refs didn't make it through to smt::solver (smt_params) in some cases. Thanks to user xor88 for pointing us in the right direction! Signed-off-by: Christoph M. Wintersteiger --- src/api/api_solver.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index ac30a0c21..c8b1723f1 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -40,6 +40,7 @@ extern "C" { params_ref p = s->m_params; mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled); s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic); + s->m_solver->updt_params(p); } static void init_solver(Z3_context c, Z3_solver s) {