diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs index 0694faabe..891ed4105 100644 --- a/src/api/dotnet/Optimize.cs +++ b/src/api/dotnet/Optimize.cs @@ -220,7 +220,7 @@ namespace Microsoft.Z3 /// /// Check satisfiability of asserted constraints. /// Produce a model that (when the objectives are bounded and - /// don't use strict inequalities) meets the objectives. + /// don't use strict inequalities) is optimal. /// /// public Status Check(params Expr[] assumptions) diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index d72a28f08..83833e36b 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -193,7 +193,7 @@ public class Optimize extends Z3Object { /** * Check satisfiability of asserted constraints. * Produce a model that (when the objectives are bounded and - * don't use strict inequalities) meets the objectives. + * don't use strict inequalities) is optimal. **/ public Status Check(Expr... assumptions) { diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 1380bd519..bb3e70875 100644 --- a/src/api/ml/z3.mli +++ b/src/api/ml/z3.mli @@ -3481,7 +3481,7 @@ sig (** Add minimization objective. *) val minimize : optimize -> Expr.expr -> handle - (** Checks whether the assertions in the context are satisfiable and solves objectives. *) + (** Check consistency and produce optimal values. *) val check : optimize -> Solver.status (** Retrieve model from satisfiable context *) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 7551d8a20..f7a99f1c2 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -8046,7 +8046,7 @@ class Optimize(Z3PPObject): Z3_optimize_pop(self.ctx.ref(), self.optimize) def check(self, *assumptions): - """Check satisfiability while optimizing objective functions.""" + """Check consistency and produce optimal values.""" assumptions = _get_args(assumptions) num = len(assumptions) _assumptions = (Ast * num)()