From c49d39af81a2a05a7cdb450175aed7a0c2ce72a9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 7 Dec 2020 21:34:57 -0800
Subject: [PATCH] perf for #4655

---
 src/smt/theory_seq.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 863e8f3f9..6f44ecf78 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1548,6 +1548,10 @@ void theory_seq::add_length(expr* e, expr* l) {
    Add length limit restrictions to sequence s.
  */
 void theory_seq::add_length_limit(expr* s, unsigned k, bool is_searching) {
+    if (m_sk.is_indexof_left(s))
+        return;
+    if (m_sk.is_indexof_right(s))
+        return;
 #if 0
     if (m_sk.is_skolem(s))
         return;