mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-30 21:57:46 +00:00
Code Activity

python type fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-11-26 09:35:07 -08:00
parent ee88359f50
commit 032a3a879b
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -4101,7 +4101,7 @@ def BV2Int(a, is_signed=False):
>>> x > BV2Int(b, is_signed=True) >>> x > BV2Int(b, is_signed=True)
x > If(b < 0, BV2Int(b) - 8, BV2Int(b)) x > If(b < 0, BV2Int(b) - 8, BV2Int(b))
>>> solve(x > BV2Int(b), b == 1, x < 3) >>> solve(x > BV2Int(b), b == 1, x < 3)
[b = 1, x = 2] [x = 2, b = 1]
""" """
if z3_debug(): if z3_debug():
_z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression") _z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
@ -10276,7 +10276,7 @@ class FPNumRef(FPRef):
""" """
def sign(self): def sign(self):
num = (ctypes.c_int)() num = (ctypes.c_bool)()
nsign = Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(num)) nsign = Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(num))
if nsign is False: if nsign is False:
raise Z3Exception("error retrieving the sign of a numeral.") raise Z3Exception("error retrieving the sign of a numeral.")