diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 3db77d7cf..71385cd1c 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1270,7 +1270,7 @@ def Distinct(*args): >>> simplify(Distinct(x, y, z)) Distinct(x, y, z) >>> simplify(Distinct(x, y, z), blast_distinct=True) - And(Not(x == y), Not(x == z), Not(y == z)) + And(Not(x == y), Not(z == x), Not(z == y)) """ args = _get_args(args) ctx = _ctx_from_ast_arg_list(args) @@ -8158,7 +8158,7 @@ def simplify(a, *arguments, **keywords): >>> simplify((x + 1)*(y + 1), som=True) 1 + x + y + x*y >>> simplify(Distinct(x, y, 1), blast_distinct=True) - And(Not(x == y), Not(x == 1), Not(y == 1)) + And(Not(y == x), Not(1 == x), Not(y == 1)) >>> simplify(And(x == 0, y == 1), elim_and=True) Not(Or(Not(x == 0), Not(y == 1))) """