diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs index 0694faabe83..891ed4105e1 100644 --- a/src/api/dotnet/Optimize.cs +++ b/src/api/dotnet/Optimize.cs @@ -220,7 +220,7 @@ public Handle AssertSoft(BoolExpr constraint, uint weight, string group) /// /// 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 d72a28f0805..83833e36bf5 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -193,7 +193,7 @@ public Handle AssertSoft(Expr constraint, String weight, String gro /** * 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 1380bd519e4..bb3e7087583 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 7551d8a2024..f7a99f1c28f 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -8046,7 +8046,7 @@ def pop(self): 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)()