mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

python: fix usage of fpa_get_numeral_significand_uint64

Browse source
This commit is contained in:
Wojciech Nawrocki 2018-06-17 13:16:36 +02:00
parent 450da5ea0c
commit 0adf66dc0a
No known key found for this signature in database
GPG key ID: 4E27C2EBC32B69B7
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/api/python/z3/z3.py
View file

@ -8858,7 +8858,10 @@ class FPNumRef(FPRef):
1.25
"""
def significand_as_long(self):
return Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast())
ptr = (ctypes.c_ulonglong * 1)()
if not Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast(), ptr):
raise Z3Exception("error retrieving the significand of a numeral.")
return ptr[0]
"""The significand of the numeral as a bit-vector expression.