From 3bf09b114af8e2d0fa3693c83e26fb7cab038811 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 7 May 2022 13:53:07 -0700 Subject: [PATCH] safe Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/UserPropagator.cs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/api/dotnet/UserPropagator.cs b/src/api/dotnet/UserPropagator.cs index 8e7831390..bab29d41b 100644 --- a/src/api/dotnet/UserPropagator.cs +++ b/src/api/dotnet/UserPropagator.cs @@ -60,7 +60,7 @@ namespace Microsoft.Z3 EqEh diseq_eh; - unsafe static void _push(voidp ctx, Z3_solver_callback cb) { + static void _push(voidp ctx, Z3_solver_callback cb) { var gch = GCHandle.FromIntPtr(ctx); var prop = (UserPropagator)gch.Target; prop.callback = cb; @@ -74,13 +74,13 @@ namespace Microsoft.Z3 prop.Pop(num_scopes); } - unsafe static voidp _fresh(voidp ctx, Z3_context new_context) { + static voidp _fresh(voidp ctx, Z3_context new_context) { var gch = GCHandle.FromIntPtr(ctx); var prop = (UserPropagator)gch.Target; throw new Z3Exception("fresh is NYI"); } - unsafe static void _fixed(voidp ctx, Z3_solver_callback cb, Z3_ast _term, Z3_ast _value) { + static void _fixed(voidp ctx, Z3_solver_callback cb, Z3_ast _term, Z3_ast _value) { var gch = GCHandle.FromIntPtr(ctx); var prop = (UserPropagator)gch.Target; var term = Expr.Create(prop.solver.Context, _term); @@ -89,14 +89,14 @@ namespace Microsoft.Z3 prop.fixed_eh(term, value); } - unsafe static void _final(voidp ctx, Z3_solver_callback cb) { + static void _final(voidp ctx, Z3_solver_callback cb) { var gch = GCHandle.FromIntPtr(ctx); var prop = (UserPropagator)gch.Target; prop.callback = cb; prop.final_eh(); } - unsafe static void _eq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) { + static void _eq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) { var gch = GCHandle.FromIntPtr(ctx); var prop = (UserPropagator)gch.Target; var s = Expr.Create(prop.solver.Context, a); @@ -105,7 +105,7 @@ namespace Microsoft.Z3 prop.eq_eh(s, t); } - unsafe static void _diseq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) { + static void _diseq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) { var gch = GCHandle.FromIntPtr(ctx); var prop = (UserPropagator)gch.Target; var s = Expr.Create(prop.solver.Context, a);