From b4290d4b3d7c021965e9ce7ee636caac0f9cac74 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Jun 2019 22:26:21 +0200 Subject: [PATCH] python regression Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 94411aa75..a7c0a099a 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1631,7 +1631,7 @@ def Xor(a, b, ctx=None): >>> Xor(p, q) Xor(p, q) >>> simplify(Xor(p, q)) - q == Not(p) + Not(p) == q """ ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx)) s = BoolSort(ctx) @@ -8159,7 +8159,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(1 == y)) + And(Not(x == y), Not(x == 1), Not(y == 1)) >>> simplify(And(x == 0, y == 1), elim_and=True) Not(Or(Not(x == 0), Not(y == 1))) """