From 7e3dfb46173e4d7e2e69bbead080cb3881ca0875 Mon Sep 17 00:00:00 2001 From: Manuel Jacob Date: Fri, 13 May 2016 23:11:15 +0200 Subject: [PATCH 1/2] Expose Z3_mk_bv2int's is_signed parameter in Python API. --- src/api/python/z3.py | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 848883ba3..624cd18f2 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -3468,7 +3468,7 @@ def is_bv_value(a): """ return is_bv(a) and _is_numeral(a.ctx, a.as_ast()) -def BV2Int(a): +def BV2Int(a, is_signed=False): """Return the Z3 expression BV2Int(a). >>> b = BitVec('b', 3) @@ -3477,6 +3477,10 @@ def BV2Int(a): >>> x = Int('x') >>> x > BV2Int(b) x > BV2Int(b) + >>> x > BV2Int(b, is_signed=False) + x > BV2Int(b) + >>> x > BV2Int(b, is_signed=True) + x > If(b < 0, BV2Int(b) - 8, BV2Int(b)) >>> solve(x > BV2Int(b), b == 1, x < 3) [b = 1, x = 2] """ @@ -3484,7 +3488,7 @@ def BV2Int(a): _z3_assert(is_bv(a), "Z3 bit-vector expression expected") ctx = a.ctx ## investigate problem with bv2int - return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), 0), ctx) + return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx) def BitVecSort(sz, ctx=None): """Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used. From 886759a58cfd2a39a4b2a87193c4019b54cef273 Mon Sep 17 00:00:00 2001 From: Teodor Vlasov Date: Sun, 15 May 2016 22:36:12 +0300 Subject: [PATCH 2/2] add DOTNET_ENABLED in parser_options of mk_*_dist --- scripts/mk_unix_dist.py | 2 +- scripts/mk_win_dist.py | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 999d495a3..0c28058ed 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -58,7 +58,7 @@ def display_help(): # Parse configuration option for mk_make script def parse_options(): - global FORCE_MK, JAVA_ENABLED, GIT_HASH + global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED path = BUILD_DIR options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 'help', diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 454bba7ca..cee8c0460 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -63,7 +63,7 @@ def display_help(): # Parse configuration option for mk_make script def parse_options(): - global FORCE_MK, JAVA_ENABLED, GIT_HASH + global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED path = BUILD_DIR options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 'help',