diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp
index fa77f0d7f6..99b409bfe0 100644
--- a/src/ast/rewriter/seq_axioms.cpp
+++ b/src/ast/rewriter/seq_axioms.cpp
@@ -443,6 +443,8 @@ namespace seq {
         expr_ref s_eq_empty = mk_eq(s, seq.str.mk_empty(s->get_sort()));
         expr_ref t_eq_empty = mk_eq_empty(t);
 
+        add_clause(mk_ge(i, -1));
+
         // |t| = 0 => |s| = 0 or indexof(t,s,offset) = -1
         // ~contains(t,s) => indexof(t,s,offset) = -1
 
diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index e368e137bd..876156262a 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -189,7 +189,9 @@ bool theory_seq::len_based_split(depeq const& e) {
     expr_ref_vector const& rs = e.rs;
     
     int offset = 0;
-    if (!has_len_offset(ls, rs, offset))
+    // Splitting on equal-length heads (offset = 0) can cause large amounts
+    // of redundant branching on indexof-heavy problems.
+    if (!has_len_offset(ls, rs, offset) || offset == 0)
         return false;
         
     TRACE(seq, tout << "split based on length\n";);
diff --git a/src/test/simplifier.cpp b/src/test/simplifier.cpp
index 3b2abf7b25..b8ed5910c3 100644
--- a/src/test/simplifier.cpp
+++ b/src/test/simplifier.cpp
@@ -232,6 +232,41 @@ static void test_sat_smt_ufbv_predicate_model_validation() {
     Z3_del_context(ctx);
 }
 
+static void test_issue_5763() {
+    Z3_context ctx = Z3_mk_context(nullptr);
+    const char* s_result =
+        Z3_eval_smtlib2_string(ctx,
+            "(set-logic QF_SLIA)\n"
+            "(declare-const db_select_s_str_1 String)\n"
+            "(assert (let ((a!1 (not (<= (str.indexof (str.substr db_select_s_str_1 7 19)\n"
+            "                                 \" where \"\n"
+            "                                 0)\n"
+            "                    0))))\n"
+            "(let ((a!2 (or a!1\n"
+            "               (= 0\n"
+            "                  (str.indexof (str.substr db_select_s_str_1 7 19) \" where \" 0)))))\n"
+            "  (and (= 0 (str.indexof db_select_s_str_1 \"select \" 0))\n"
+            "       (<= 0 (str.indexof (str.substr db_select_s_str_1 7 19) \" from \" 0))\n"
+            "       (not a!2)\n"
+            "       (= (str.substr (str.substr db_select_s_str_1 7 19) 10 9) \"inventory\")))))\n"
+            "(check-sat)\n");
+    ENSURE(std::strstr(s_result, "sat") != nullptr);
+
+    const char* bv_result =
+        Z3_eval_smtlib2_string(ctx,
+            "(declare-const my_fn_a_int_1 Int)\n"
+            "(declare-const my_fn_b_int_2 Int)\n"
+            "(assert (let ((a!1 (bvnot (bvor (bvnot ((_ int2bv 64) my_fn_a_int_1))\n"
+            "                        (bvnot ((_ int2bv 64) my_fn_b_int_2))))))\n"
+            "(let ((a!2 (bvor (bvnot (bvor ((_ int2bv 64) my_fn_a_int_1)\n"
+            "                              ((_ int2bv 64) my_fn_b_int_2)))\n"
+            "                 a!1)))\n"
+            "  (not (= 0 (bv2int (bvnot a!2)))))))\n"
+            "(check-sat)\n");
+    ENSURE(std::strstr(bv_result, "sat") != nullptr);
+    Z3_del_context(ctx);
+}
+
 void tst_simplifier() {
 
     test_array();
@@ -240,4 +275,5 @@ void tst_simplifier() {
     test_bool();
     test_skolemize_bug();
     test_sat_smt_ufbv_predicate_model_validation();
+    test_issue_5763();
 }