From 8f798fef1a10706f9871f7baff12b564326d6fc7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Mar 2017 08:24:12 -0700 Subject: [PATCH] fix python interface for string extract to take symbolic indices per bug report from Kun Wei Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 16d7fbb5f..568ffe9a2 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -3701,12 +3701,8 @@ def Extract(high, low, a): high = StringVal(high) if is_seq(high): s = high - offset = _py2expr(low, high.ctx) - length = _py2expr(a, high.ctx) - - if __debug__: - _z3_assert(is_int(offset) and is_int(length), "Second and third arguments must be integers") - return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx) + offset, length = _coerce_exprs(low, a, s.ctx) + return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx) if __debug__: _z3_assert(low <= high, "First argument must be greater than or equal to second argument") _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0, "First and second arguments must be non negative integers")