From 0093157bb90ed056940c354ba7075d4514443be3 Mon Sep 17 00:00:00 2001
From: Phillip Schanely <pschanely+gitcmt@gmail.com>
Date: Tue, 13 Aug 2019 06:12:14 -0400
Subject: [PATCH] Handle dynamic sort of Nth()'s return value in the Python API

---
 src/api/python/z3/z3.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 594d19d05..22cc757e3 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -9976,7 +9976,7 @@ class SeqRef(ExprRef):
     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):