From 9c6b29164dff7b42683ce3b84b0c9c9adbbf2b08 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 15 Jun 2021 12:31:21 -0500 Subject: [PATCH] #5337 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 510d517be..62e3fbd79 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -4088,7 +4088,13 @@ def Concat(*args): def Extract(high, low, a): - """Create a Z3 bit-vector extraction expression, or create a string extraction expression. + """Create a Z3 bit-vector extraction expression. + Extract is overloaded to also work on sequence extraction. + The functions SubString and SubSeq are redirected to Extract. + For this case, the arguments are reinterpreted as: + high - is a sequence (string) + low - is an offset + a - is the length to be extracted >>> x = BitVec('x', 8) >>> Extract(6, 2, x)