From a352a6638a93f1490df66ded3abc97810838a9dc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 26 Mar 2021 12:20:31 -0700
Subject: [PATCH] fix #5126

---
 src/ast/rewriter/seq_skolem.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ast/rewriter/seq_skolem.cpp b/src/ast/rewriter/seq_skolem.cpp
index 8fae87643..56c169ef6 100644
--- a/src/ast/rewriter/seq_skolem.cpp
+++ b/src/ast/rewriter/seq_skolem.cpp
@@ -112,7 +112,7 @@ decompose_main:
     }
     else if (is_skolem(m_tail, e) && a.is_numeral(to_app(e)->get_arg(1), r)) {        
         expr* s = to_app(e)->get_arg(0);        
-        expr* idx = a.mk_int(r.get_unsigned() + 1);
+        expr* idx = a.mk_int(r + 1);
         head = seq.str.mk_unit(seq.str.mk_nth_i(s, idx));
         tail = mk(m_tail, s, idx);
         m_rewrite(head);