perf for #4655

Z3Prover · Dec 8, 2020 · c49d39a · c49d39a
1 parent f5f980f
commit c49d39a
Showing 1 changed file with 4 additions and 0 deletions.
diff --git 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;