From 34da0a32b9a9b97b5e5044d32e54bf1b3a3bdcc9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andres=20N=C3=B6tzli?= Date: Wed, 16 Mar 2016 17:12:45 -0700 Subject: [PATCH] [Z3py] Fix error in FPRef.__neg__() `FPRef.__neg__()` did not work previously because it tried to construct an FPRef from an FPRef (`fpNeg()` already returns an FPRef). --- src/api/python/z3.py | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 5727d2dfb..374c71be4 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -8178,8 +8178,13 @@ class FPRef(ExprRef): return self def __neg__(self): - """Create the Z3 expression `-self`.""" - return FPRef(fpNeg(self)) + """Create the Z3 expression `-self`. + + >>> x = FP('x', Float32()) + >>> -x + -x + """ + return fpNeg(self) def __div__(self, other): """Create the Z3 expression `self / other`.