diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 3a8800f1d..305733aa7 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -8824,7 +8824,7 @@ def _check_fp_args(a, b): _z3_assert(is_fp(a) or is_fp(b), "At least one of the arguments must be a Z3 floating-point expression") def fpLT(a, b, ctx=None): - """Create the Z3 floating-point expression `other <= self`. + """Create the Z3 floating-point expression `other < self`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpLT(x, y) @@ -8846,7 +8846,7 @@ def fpLEQ(a, b, ctx=None): return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx) def fpGT(a, b, ctx=None): - """Create the Z3 floating-point expression `other <= self`. + """Create the Z3 floating-point expression `other > self`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpGT(x, y) @@ -8857,11 +8857,9 @@ def fpGT(a, b, ctx=None): return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx) def fpGEQ(a, b, ctx=None): - """Create the Z3 floating-point expression `other <= self`. + """Create the Z3 floating-point expression `other >= self`. >>> x, y = FPs('x y', FPSort(8, 24)) - >>> x + y - x + y >>> fpGEQ(x, y) x >= y >>> (x >= y).sexpr() @@ -8870,7 +8868,7 @@ def fpGEQ(a, b, ctx=None): return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx) def fpEQ(a, b, ctx=None): - """Create the Z3 floating-point expression `other <= self`. + """Create the Z3 floating-point expression `fpEQ(other, self)`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpEQ(x, y) @@ -8881,7 +8879,7 @@ def fpEQ(a, b, ctx=None): return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx) def fpNEQ(a, b, ctx=None): - """Create the Z3 floating-point expression `other <= self`. + """Create the Z3 floating-point expression `Not(fpEQ(other, self))`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpNEQ(x, y)