diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index afdca7464..b8ec74d18 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -3572,15 +3572,19 @@ def Concat(*args):
     if __debug__:
         _z3_assert(sz >= 2, "At least two arguments expected.")
 
-    ctx = args[0].ctx
-
-    if is_seq(args[0]):
-       if __debug__:
-         _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
-       v = (Ast * sz)()
-       for i in range(sz):
+    ctx = None
+    for a in args:
+        if is_expr(a):
+            ctx = a.ctx
+            break
+    if is_seq(args[0]) or isinstance(args[0], str):
+        args = [_coerce_seq(s, ctx) for s in args]
+        if __debug__:
+            _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.")
+        v = (Ast * sz)()
+        for i in range(sz):
             v[i] = args[i].as_ast()
-       return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
+        return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
 
     if is_re(args[0]):
        if __debug__:
@@ -9066,7 +9070,12 @@ class SeqRef(ExprRef):
     def __add__(self, other):
         return Concat(self, other)
 
+    def __radd__(self, other):
+        return Concat(other, self)
+
     def __getitem__(self, i):
+        if _is_int(i):
+            i = IntVal(i, self.ctx)
         return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
 
     def is_string(self):