mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
[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).
This commit is contained in:
parent
6b2d84b2be
commit
34da0a32b9
|
@ -8178,8 +8178,13 @@ class FPRef(ExprRef):
|
||||||
return self
|
return self
|
||||||
|
|
||||||
def __neg__(self):
|
def __neg__(self):
|
||||||
"""Create the Z3 expression `-self`."""
|
"""Create the Z3 expression `-self`.
|
||||||
return FPRef(fpNeg(self))
|
|
||||||
|
>>> x = FP('x', Float32())
|
||||||
|
>>> -x
|
||||||
|
-x
|
||||||
|
"""
|
||||||
|
return fpNeg(self)
|
||||||
|
|
||||||
def __div__(self, other):
|
def __div__(self, other):
|
||||||
"""Create the Z3 expression `self / other`.
|
"""Create the Z3 expression `self / other`.
|
||||||
|
|
Loading…
Reference in a new issue