From c7fd74e8adc6be5eca0f153ddb781927f98210e0 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 2 Jun 2015 12:45:55 +0100 Subject: [PATCH] Fixed FPA Python doctest --- src/api/python/z3.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 9ac9da3e8..f6a617317 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -8205,12 +8205,13 @@ def FPs(names, fpsort, ctx=None): >>> x, y, z = FPs('x y z', FPSort(8, 24)) >>> x.sort() + FPSort(8, 24) >>> x.sbits() 24 >>> x.ebits() 8 - >>> simplify(Product(x, y, z)) - x*y*z + >>> fpMul(RNE(), fpAdd(RNE(), x, y), z) + fpMul(RNE(), fpAdd(RNE(), x, y), z) """ ctx = z3._get_ctx(ctx) if isinstance(names, str):