Handle dynamic sort of Nth()'s return value in the Python API

Author: Phillip Schanely

src/api/python/z3/z3.py

@@ -9976,7 +9976,7 @@ def __radd__(self, other):
     def __getitem__(self, i):
         if _is_int(i):
             i = IntVal(i, self.ctx)
-        return SeqRef(Z3_mk_seq_nth(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
+        return _to_expr_ref(Z3_mk_seq_nth(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx)
 
     def at(self, i):
         if _is_int(i):