From 31895440507aef1eb16dd8d2ddd205e059e1075d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Jun 2022 21:05:51 -0700 Subject: [PATCH] next split Signed-off-by: Nikolaj Bjorner --- src/api/dotnet/UserPropagator.cs | 9 +++++++++ src/api/java/NativeStatic.txt | 1 + 2 files changed, 10 insertions(+) diff --git a/src/api/dotnet/UserPropagator.cs b/src/api/dotnet/UserPropagator.cs index bfd7887dd..0b0e5a57f 100644 --- a/src/api/dotnet/UserPropagator.cs +++ b/src/api/dotnet/UserPropagator.cs @@ -298,6 +298,15 @@ namespace Microsoft.Z3 } } + + /// + /// Set the next decision + /// + public void NextSplit(Expr e, uint idx, Z3_lbool phase) + { + Native.Z3_solver_next_split(ctx.nCtx, this.callback, e.NativeObject, idx, phase); + } + /// /// Track assignments to a term /// diff --git a/src/api/java/NativeStatic.txt b/src/api/java/NativeStatic.txt index 2cd718627..657050951 100644 --- a/src/api/java/NativeStatic.txt +++ b/src/api/java/NativeStatic.txt @@ -76,3 +76,4 @@ DLL_VIS JNIEXPORT void JNICALL Java_com_microsoft_z3_Native_setInternalErrorHand { Z3_set_error_handler((Z3_context)a0, Z3JavaErrorHandler); } +