diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs
index 891ed4105..3bc06de16 100644
--- a/src/api/dotnet/Optimize.cs
+++ b/src/api/dotnet/Optimize.cs
@@ -148,6 +148,28 @@ namespace Microsoft.Z3
Native.Z3_optimize_assert(Context.nCtx, NativeObject, a.NativeObject);
}
}
+
+ ///
+ /// Assert a constraint into the optimize solver, and track it (in the unsat) core
+ /// using the Boolean constant p.
+ ///
+ ///
+ /// This API is an alternative to with assumptions for extracting unsat cores.
+ /// Both APIs can be used in the same solver. The unsat core will contain a combination
+ /// of the Boolean variables provided using
+ /// and the Boolean literals
+ /// provided using with assumptions.
+ ///
+ public void AssertAndTrack(BoolExpr constraint, BoolExpr p)
+ {
+ Debug.Assert(constraint != null);
+ Debug.Assert(p != null);
+ Context.CheckContextMatch(constraint);
+ Context.CheckContextMatch(p);
+
+ Native.Z3_optimize_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
+ }
+
///
/// Handle to objectives returned by objective functions.
///