From 14c19fe9283968d295ba2106a32584de6be52ba7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 15 Jan 2016 10:39:21 +0530 Subject: [PATCH] add parameter validation to sequence expressions Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 0626d2f3c..323e57c79 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -9095,6 +9095,10 @@ def _coerce_seq(s, ctx=None): if isinstance(s, str): ctx = _get_ctx(ctx) s = StringVal(s, ctx) + if not is_expr(s): + raise Z3Exception("Non-expression passed as a sequence") + if not is_seq(s): + raise Z3Exception("Non-sequence passed as a sequence") return s def _get_ctx2(a, b, ctx=None):