diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp index e368e137bd..03cdd6c703 100644 --- a/src/smt/seq_eq_solver.cpp +++ b/src/smt/seq_eq_solver.cpp @@ -189,7 +189,7 @@ 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)) + if (!has_len_offset(ls, rs, offset) || offset == 0) return false; TRACE(seq, tout << "split based on length\n";);