From 1147037a990022ee8e1e962facae67153d565765 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 2 Jan 2016 22:54:49 -0800 Subject: [PATCH] seq API Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 507e9bfee..802108163 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -9015,12 +9015,13 @@ def Empty(s): >>> print(e) "" >>> e2 = String("") - >>> print(e == e2) + >>> print(e.eq(e2)) True >>> e3 = Empty(SeqSort(IntSort())) >>> print(e3) + seq.empty """ - return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.as_ast()), s.ctx) + return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx) def Unit(a): """Create a singleton sequence"""