From 8cc3ba5a8b8ced685669d43ec315bd282a13269d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 4 Mar 2016 13:09:42 +0000 Subject: [PATCH] fixed FP Python doctest examples --- src/api/python/z3.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 3a4276dfd..088cd0d4d 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -8524,11 +8524,11 @@ def FPVal(sig, exp=None, fps=None, ctx=None): >>> v = FPVal(-2.25, FPSort(8, 24)) >>> v -1.125*(2**1) - >>> v = FPVal(-0.0, FPSort(8, 24)) + >>> FPVal(-0.0, FPSort(8, 24)) -0.0 - >>> v = FPVal(0.0, FPSort(8, 24)) + >>> FPVal(0.0, FPSort(8, 24)) +0.0 - >>> v = FPVal(+0.0, FPSort(8, 24)) + >>> FPVal(+0.0, FPSort(8, 24)) +0.0 """ ctx = _get_ctx(ctx) @@ -8911,7 +8911,7 @@ def fpNEQ(a, b, ctx=None): >>> fpNEQ(x, y) Not(fpEQ(x, y)) >>> (x != y).sexpr() - '(not (fp.eq x y))' + '(distinct x y)' """ return Not(fpEQ(a, b, ctx))