From 32164b6c7f307b93118fa257bebbd0db6ea3ee56 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 24 Mar 2019 13:10:11 -0700
Subject: [PATCH] fix python doc regressions

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/python/z3/z3.py | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 8a7053deb..173119011 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -3841,7 +3841,7 @@ def Extract(high, low, a):
     >>> Extract(6, 2, x).sort()
     BitVec(5)
     >>> simplify(Extract(StringVal("abcd"),2,1))
-    c
+    "c"
     """
     if isinstance(high, str):
         high = StringVal(high)
@@ -10051,10 +10051,10 @@ def Empty(s):
     True
     >>> e3 = Empty(SeqSort(IntSort()))
     >>> print(e3)
-    seq.empty
+    Empty(Seq(Int))
     >>> e4 = Empty(ReSort(SeqSort(IntSort())))
     >>> print(e4)
-    re.empty
+    Empty(ReSort(Seq(Int)))
     """
     if isinstance(s, SeqSortRef):
        return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
@@ -10066,10 +10066,10 @@ def Full(s):
     """Create the regular expression that accepts the universal language
     >>> e = Full(ReSort(SeqSort(IntSort())))
     >>> print(e)
-    re.all
+    Full(ReSort(Int))
     >>> e1 = Full(ReSort(StringSort()))
     >>> print(e1)
-    rel.all
+    Full(ReSort(String))
     """
     if isinstance(s, ReSortRef):
        return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx)
@@ -10131,7 +10131,7 @@ def Replace(s, src, dst):
     """Replace the first occurrence of 'src' by 'dst' in 's'
     >>> r = Replace("aaa", "a", "b")
     >>> simplify(r)
-    baa
+    "baa"
     """
     ctx = _get_ctx2(dst, s)
     if ctx is None and is_expr(src):
@@ -10276,7 +10276,6 @@ def Union(*args):
 def Intersect(*args):
     """Create intersection of regular expressions.
     >>> re = Intersect(Re("a"), Re("b"), Re("c"))
-    Intersect(Re("a"), Re("b"), Re("c"))
     """
     args = _get_args(args)
     sz = len(args)