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);
}
+